CS 463
Homework 6 - Simply Typed Lambda Calculus
Solutions Spring 2024
================================================================================

1.1    2*(3+4)


                  ------Ty-ℤ -------Ty-ℤ
                  {}⊢3: ℤ    {}⊢4:ℤ
-----------Ty-ℤ   ------------------Ty-Add
{} ⊢ 2 : ℤ        {} ⊢ (3+4) : ℤ
------------------------------------ Ty-Mul
{} ⊢ 2*(3+4) : ℤ

================================================================================

1.2    if (0>1) 2 3


-------Ty-ℤ -------Ty-ℤ
{}⊢0:ℤ      {}⊢1:ℤ
--------------------Ty-GT  --------Ty-ℤ  -------Ty-ℤ
{}⊢(0>1):𝔹                 {}⊢2:ℤ        {}⊢3:ℤ
------------------------------------------------Ty-If
{} ⊢ if (0>1) 2 3 : ℤ



================================================================================

1.3    (((λx:ℤ.λy:ℤ.x+y) 8) 9)


------------------Ty-Var  ------------------Ty-Var
{(x,ℤ),(y,ℤ)}⊢x:ℤ        {(x,ℤ),(y,ℤ)}⊢y:ℤ
-----------------------------------------------Ty-Add
{(x,ℤ),(y,ℤ)}⊢(x+y): ℤ
-------------------------Ty-λ
{(x,ℤ)}⊢(λy:ℤ.x+y): ℤ→ℤ
-------------------------Ty-λ  -------Ty-ℤ
{}⊢(λx:ℤ.λy:ℤ.x+y): ℤ→(ℤ→ℤ)    {}⊢8:ℤ
--------------------------------------------Ty-App  ---------- Ty-ℤ
{} ⊢ ((λx:ℤ.λy:ℤ.x+y) 8) : ℤ → ℤ                    {}⊢ 9 : ℤ
-------------------------------------------------------------- Ty-App
{}⊢ (((λx:ℤ.λy:ℤ.x+y) 8) 9) : ℤ


================================================================================

1.4    ((λx:ℤ.x+1) 5)


-------------Ty-Var  -------------Ty-ℤ
{(x,ℤ)}⊢x:ℤ          {(x,ℤ)}⊢1:ℤ
---------------------------------Ty-Add
{(x,ℤ)}⊢(x+1) : ℤ
---------------------Ty-λ  ---------Ty-ℤ
{} ⊢ (λx:ℤ.x+1) : ℤ→ℤ      {}⊢5: ℤ
------------------------------------- Ty-App
{} ⊢ ((λx:ℤ.x+1) 5) : ℤ


================================================================================

1.5    (head ( nil ⟦𝔹⟧ ))


---------------- Ty-nil
{}⊢(nil ⟦𝔹⟧) : ⟦𝔹⟧
--------------------------- Ty-head
{}⊢(head ( nil ⟦𝔹⟧ )) : 𝔹

================================================================================

2.1   cons true (nil ⟦ℤ⟧)


------------Ty-true  ---------------Ty-nil
{}⊢ true : 𝔹         {}⊢(nil⟦ℤ⟧) : ⟦ℤ⟧
----------------------------------------- Ty-cons
{} ⊢ cons true (nil ⟦ℤ⟧) : XXX


Ty-cons needs the second subterm's type to be a list containing items of the
first subterm's type, but ⟦ℤ⟧ doesn't contain 𝔹's.

================================================================================

2.2.  ((λx:ℤ.x>2) true)


------------Ty-Var  ------------Ty-ℤ
{(x,ℤ)}⊢x:ℤ         {(x,ℤ)}⊢2:ℤ
--------------------------------Ty-GT
{(x,ℤ)} ⊢ (x>2) : 𝔹
-------------------------Ty-λ  ------------- Ty-true
{} ⊢ (λx:ℤ.x>2) :  ℤ→𝔹         {}⊢ true : 𝔹
-------------------------------------------- Ty-App
{}⊢ ((λx:ℤ.x>2) true) : XXX

Ty-App sees a function that needs a ℤ argument, but it's receiving a 𝔹.

================================================================================

3.1

                   Γ ⊢ t1 : T1
Ty-just     ------------------------
            Γ ⊢ just t1  :  Maybe T1


               
Ty-nothing  --------------------------
            Γ ⊢ nothing T1 : Maybe T1



                Γ ⊢  t1 : Maybe T1
Ty-isjust   -------------------------
                Γ ⊢ isjust t1 : 𝔹


                Γ ⊢ t1 : Maybe T1
Ty-unjust   -------------------------
               Γ ⊢ unjust t1  :  T1



================================================================================

3.2

                Γ ⊢ t1 : T1
Ty-left     ------------------------------
            Γ ⊢ left t1 T2 : Either T1 T2


                Γ ⊢ t2 : T2
Ty-right    ------------------------------
            Γ ⊢ right T1 t2 : Either T1 T2


            Γ ⊢ t : Either T1 T2
Ty-isleft   ---------------------
            Γ ⊢ isleft t : 𝔹


            Γ ⊢ t : Either T1 T2
Ty-isright  ---------------------
            Γ ⊢ isright t : 𝔹


            Γ ⊢ t : Either T1 T2
Ty-getleft  ---------------------
            Γ ⊢ getleft t : T1


            Γ ⊢ t : Either T1 T2
Ty-getright ---------------------
            Γ ⊢ getright t : T2


================================================================================
4. encodings

nand = λx:𝔹. λy:𝔹. if x (~y) true

thrice = λf:ℤ→ℤ. λn:ℤ. (f (f (f n)))

cubed = λx:ℤ. x*x*x

modify = λe:Either ℤ 𝔹. if (isleft e)
                           (left ((getleft t)+1) 𝔹)
                           (right ℤ (~ (getright e)))

safeAdd = λm1:Maybe ℤ. λm2:Maybe ℤ. (if (isjust m1) (getjust m1) 0)
                                    +
                                    (if (isjust m2) (getjust m2) 0)



all = fix (λself:⟦𝔹⟧→𝔹.
            λxs:⟦𝔹⟧. if (isnil xs) true (if (~(head xs)) false (self (tail xs))))

sumlist = fix (λself:⟦ℤ⟧→ℤ.
                λxs:⟦ℤ⟧. if (isnil xs) 0 ((head xs) + (self (tail xs))))

takeN = fix (λself:ℤ→⟦ℤ⟧→⟦ℤ⟧. λn:ℤ. λxs:⟦ℤ⟧.
                if (n=0) (nil ⟦ℤ⟧)
                  (if (isnil xs) (nil ⟦ℤ⟧)
                    (cons (head xs) (self (n-1) (tail xs)))))

filter = fix (λself:(ℤ→𝔹)→⟦ℤ⟧→⟦ℤ⟧.λf:ℤ→𝔹.λxs:⟦ℤ⟧.
                if (isnil xs) (nil ⟦ℤ⟧)
                  (if (f (head xs))
                      (cons (head xs) (self (tail xs)))
                      (                self (tail xs))))

zipwith = fix (λself:(ℤ→ℤ→ℤ)→⟦ℤ⟧→⟦ℤ⟧→⟦ℤ⟧.
                λf:ℤ→ℤ→ℤ. λxs:⟦ℤ⟧. λys:⟦ℤ⟧. 
                    if (isnil xs) (nil ⟦ℤ⟧)
                     (if (isnil ys) (nil ⟦ℤ⟧)
                      (cons (f (head xs) (head ys))
                            (self f (tail xs) (tail ys)))))


================================================================================

5. extra credit.


maxlist = fix ( λself:⟦ℤ⟧ → Maybe ℤ. λxs:⟦ℤ⟧.
              if (isnil xs)
                 (nothing ℤ)
                 (if (isnil (tail xs))
                     (just  (head xs))
                     (if ((head xs) > (unjust (self (tail xs))))
                         (just (head xs))
                         (self (tail xs)))))



================================================================================