STLC Slides: Practice Problem Solutions

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

Practice Problems: Encodings

and  = λa:𝔹.λb:𝔹.if a b a
or   = λa:𝔹.λb:𝔹.if a a b
ge   = λa:ℤ.λb:ℤ. or (a>b) (a=b)
inc  = λa:ℤ.a+1
max3 = λx:ℤ.λy:ℤ.λz:ℤ. if (and (ge x y) (ge x z))
                          x
                          (if (ge y z) y z)

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

Practice Problems: Proof Trees

--------------------------------------------------------------------------------
#1.    ((λx:ℤ.x) ((λn:ℤ.n) 10))

                           ---------------Ty-var
                            {(n,ℤ)}⊢n:ℤ
-------------Ty-var        -----------------Ty-λ   ----------Ty-Int
 {(x,ℤ)}⊢x:ℤ                {}⊢(λn:ℤ.n):ℤ→ℤ         {}⊢10:ℤ
---------------------Ty-λ  ----------------------------------Ty-App
    {}⊢(λx:ℤ.x): ℤ→ℤ        {}⊢((λn:ℤ.n) 10)) : ℤ
-------------------------------------------------------------Ty-App
{}⊢((λx:ℤ.x) ((λn:ℤ.n) 10)) : ℤ



--------------------------------------------------------------------------------
#2.    ((λx:ℤ.if true x (x+1)) 5)

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



--------------------------------------------------------------------------------
#3.    (λf:ℤ→ℤ. λx:ℤ.f x)


----------------------Ty-Var   ---------------------Ty-Var
{(f:ℤ→ℤ),(x:ℤ)}⊢f:ℤ→ℤ           {(f:ℤ→ℤ),(x:ℤ)}⊢x:ℤ
----------------------------------------------------Ty-App
{(f:ℤ→ℤ),(x:ℤ)}⊢(f x) : ℤ
----------------------------Ty-λ
{(f:ℤ→ℤ)}⊢(λx:ℤ.f x) : ℤ→ℤ
----------------------------------Ty-λ
{}⊢(λf:ℤ→ℤ. λx:ℤ.f x) : (ℤ→ℤ)→(ℤ→ℤ)


--------------------------------------------------------------------------------
#4.    (((λx:ℤ. λy:ℤ.x+y) 5) 8)

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


--------------------------------------------------------------------------------
#5.    (3 5)

-------Ty-Int  --------Ty-Int
{}⊢3:ℤ         {}⊢5:ℤ
------------------------Ty-App
{}⊢(3 5): <FAILURE>

Ty-App cannot be used when needed, because its first subterm must be a
function-type but 3 is an ℤ.


--------------------------------------------------------------------------------
#6.    ((λx:ℤ.x+1) true)

-------------Ty-Var  -------------Ty-Int
{(x,ℤ)}⊢x:ℤ           {(x,ℤ)}⊢1:ℤ
----------------------------------Ty-Add
{(x,ℤ)}⊢(x+1): ℤ
----------------------------------Ty-λ   -----------Ty-True
{}⊢(λx:ℤ.x+1): ℤ→ℤ                        {}⊢true:𝔹
----------------------------------Ty-App
{}⊢((λx:ℤ.x+1) true) : <FAILURE>

Ty-App cannot be used when needed, because its first subterm is a function
expecting an ℤ argument, but the second subterm provided is a 𝔹 argument.


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

Practice Problems - Encodings

and = λx:𝔹. λy:𝔹. if x y false

or  = λx:𝔹. λy:𝔹. if x true y

ge  = λx:ℤ. λy:ℤ. if (x>y) true (x=y)

inc = λx:ℤ. x+1

max3 = λx:ℤ. λy:ℤ. λz:ℤ. if (or (ge x y) (ge x z))
                             x
                            (if (ge y z) y z)

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

Practice Problems - Pairs + Proof Trees

--------------------------------------------------------------------------------

#1. pair true 4

----------Ty-true  -------Ty-Int
{}|-true: 𝔹        {}|-4:ℤ
---------------------------Ty-Pair
{} |- pair true 4 : ⦅𝔹,ℤ⦆


--------------------------------------------------------------------------------

#2.  fst (pair 3 true)


------TyInt   ----------Ty-true
{}⊢3:ℤ        {}⊢true:𝔹
------------------------Ty-pair
{}⊢(pair 3 true):⦅ℤ,𝔹⦆
-------------------------Ty-fst
{}⊢fst (pair 3 true) : ℤ


--------------------------------------------------------------------------------

#3. snd p, with Γ={(p, ⦅𝔹,ℤ⦆)}.


----------------------------- Ty-Var
{(p,⦅𝔹,ℤ⦆)} |- p : ⦅𝔹,ℤ⦆
----------------------------- Ty-Snd
{(p,⦅𝔹,ℤ⦆)} |- snd p : ℤ


Notice we don't actually care/get to see what p's term was...

--------------------------------------------------------------------------------

#4.  λp:⦅ℤ,𝔹⦆. if (snd p) (fst p) 0


-------------------Ty-Var   -------------------Ty-Var
{(p,⦅ℤ,𝔹⦆)}⊢p:⦅ℤ,𝔹⦆          {(p,⦅ℤ,𝔹⦆)}⊢p:⦅ℤ,𝔹⦆
-------------------Ty-snd   ---------------------Ty-fst   ----------------Ty-Int
{(p,⦅ℤ,𝔹⦆)}⊢(snd p):𝔹       {(p,⦅ℤ,𝔹⦆)}⊢(fst p):ℤ          {(p,⦅ℤ,𝔹⦆)}⊢0:ℤ
--------------------------------------------------------------------------Ty-If
                  {(p,⦅ℤ,𝔹⦆)}⊢ (if (snd p) (fst p) 0) :  ℤ
--------------------------------------------------------------------------Ty-λ
                {}⊢ (λp:⦅ℤ,𝔹⦆. (if (snd p) (fst p) 0)) : ⦅ℤ,𝔹⦆→ℤ


--------------------------------------------------------------------------------

#5.  (pair (x:ℤ.x+1) (\f:ℤ→ℤ.f 1))


------------TyVar  -------------Ty-Z    ------------------Ty-Var  ---------------Ty-Z
{(x,ℤ)}|-x:ℤ        {(x,ℤ)}|-1:ℤ        {(f,ℤ→ℤ)}|-f:ℤ→ℤ          {(f,ℤ→ℤ)}|-1:ℤ
--------------------------------Ty-Add  ------------------------------------------Ty-App
{(x,ℤ)}|-(x+1): ℤ                       {(f,ℤ→ℤ)}|-(f 1): ℤ
------------------Ty-λ                  ------------------------------Ty-λ
{}|-(λx:ℤ.x+1): ℤ→ℤ                     {}|-(λf:ℤ→ℤ.f 1): (ℤ→ℤ)→ℤ
----------------------------------------------------------------------Ty-pair
{}|- (pair (λx:ℤ.x+1) (λf:ℤ→ℤ.f 1)) : (ℤ→ℤ , (ℤ→ℤ)→ℤ)



--------------------------------------------------------------------------------

#1.failure:     fst (λx:ℤ.pair x x)


------------Ty-Var ------------Ty-Var
{(x,Z)}|-x:Z       {(x,Z)}|-x:Z
-------------------------------Ty-Pair
{(x,Z)}|-(pair x x) : (Z,Z)
-----------------------------Ty-λ
{}|-(\x:Z.pair x x): Z -> (Z,Z)
--------------------------------Ty-Fst
{}|- fst (\x:Z.pair x x) : ??


Error: Ty-Fst needs the subterm to be a pair type;
we found a function here (Z -> (Z,Z)).


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

Practice Problems - Recursion

--------------------------------------------------------------------------------
#1.    (fix (λself:ℤ→ℤ. λn:ℤ.if (n<2) 1 (n*(self (n-1)))))

(full proof tree is shown)

Note how we keep truncating the environments, e.g. {(n,ℤ)...}, to only include
variables that are actually present in the term being considered. This helps to
keep our tree simpler, but an implementation wouldn't bother with this extra
filtering effort.

(open this in a code editor or something that won't line-wrap the text).

                                                                                                                      ---------------Ty-Var  ----------Ty-Int        
                                                                                                                       {(n,ℤ)...}⊢n:ℤ        {...}⊢1:ℤ
                                                                                   -------------------------Ty-Var    ---------------------------------Ty-Sub
                                                                                    {(self,ℤ→ℤ)...}⊢self:ℤ→ℤ           {(self,ℤ→ℤ),(n,ℤ)}⊢(n-1):ℤ
--------------Ty-Var  ---------Ty-Int                       ---------------Ty-Var  -----------------------------------------------------------------Ty-App
{(n,ℤ)...}⊢n:ℤ        {...}⊢2:ℤ                             {(n,ℤ)...}⊢n:ℤ         {(self,ℤ→ℤ),(n,ℤ)}⊢(self (n-1)):ℤ
--------------------------------Ty-LT     ---------Ty-Int   ---------------------------------------------------------------------Ty-Mul
{(n,ℤ)...} ⊢(n<2): 𝔹                      {...}⊢1:ℤ          {(self,ℤ→ℤ),(n,ℤ)}⊢:(n*(self (n-1)))):ℤ
--------------------------------------------------------------------------------------------------------------Ty-If
{(self,ℤ→ℤ),(n,ℤ)} ⊢(if (n<2) 1 (n*(self (n-1)))) : ℤ
---------------------------------------------------------------Ty-λ
{(self,ℤ→ℤ)} ⊢ (λn:ℤ.if (n<2) 1 (n*(self (n-1)))) : ℤ→ℤ
---------------------------------------------------------------Ty-λ
{}⊢(λself:ℤ→ℤ. (λn:ℤ.if (n<2) 1 (n*(self (n-1))))) : (ℤ→ℤ)→(ℤ→ℤ)
---------------------------------------------------------------Ty-Fix
{}⊢(fix (λself:ℤ→ℤ. λn:ℤ.if (n<2) 1 (n*(self (n-1))))) : (ℤ→ℤ)




--------------------------------------------------------------------------------
#2.

factorial = fix ( λself:ℤ→ℤ.
                     λn:ℤ.
                         if (n<2) 1 (n*(self (n-1)))
                )

--------------------------------------------------------------------------------
#3.

fibonacci = fix ( λself:ℤ→ℤ.
                      λn:ℤ.
                          if (n<2) n ((self (n-1)) + (self (n-2)))
                )

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

Practice Problems - Lists

--------------------------------------------------------------------------------
#1.    (head (if true (cons 5 (nil ⟦ℤ⟧)) (nil ⟦ℤ⟧)))


                    -------Ty-Int   ---------------Ty-Nil
                    {}⊢5:ℤ          {}⊢(nil ⟦ℤ⟧):⟦ℤ⟧
----------Ty-True   -------------------------------Ty-Cons   ------------------Ty-Nil
{}⊢true:𝔹           {}⊢(cons 5 (nil ⟦ℤ⟧)):⟦ℤ⟧                 {}⊢(nil ⟦ℤ⟧) : ⟦ℤ⟧
-------------------------------------------------------------------------------Ty-If
{}⊢(if true (cons 5 (nil ⟦ℤ⟧)) (nil ⟦ℤ⟧)) : ⟦ℤ⟧
-----------------------------------------------------Ty-Head
{}⊢(head (if true (cons 5 (nil ⟦ℤ⟧)) (nil ⟦ℤ⟧))) : ℤ



--------------------------------------------------------------------------------
#2.    (head (tail (cons 10 (cons 12 (cons 13 (nil ⟦ℤ⟧))))))


                                   ---------Ty-Int   --------------------Ty-Nil
                                   {}⊢13:ℤ           {}⊢(nil ⟦ℤ⟧) : ⟦ℤ⟧
                 ---------Ty-Int   --------------------------------------Ty-Cons
                 {}⊢12:ℤ           {}⊢(cons 13 (nil ⟦ℤ⟧)) : ⟦ℤ⟧
--------Ty-Int   ----------------------------------------------Ty-Cons
{}⊢10:ℤ          {}⊢(cons 12 (cons 13 (nil ⟦ℤ⟧))) : ⟦ℤ⟧
-------------------------------------------------------Ty-Cons
{}⊢(cons 10 (cons 12 (cons 13 (nil ⟦ℤ⟧)))) : ⟦ℤ⟧
-------------------------------------------------------Ty-Tail
{}⊢(tail (cons 10 (cons 12 (cons 13 (nil ⟦ℤ⟧))))) : ⟦ℤ⟧
-------------------------------------------------------------Ty-Head
{}⊢(head (tail (cons 10 (cons 12 (cons 13 (nil ⟦ℤ⟧)))))) : ℤ


--------------------------------------------------------------------------------
#3.

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

--------------------------------------------------------------------------------
#4.

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

--------------------------------------------------------------------------------
#5.

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

-- note, it's possible to get an out-of-bounds error!
-- even though it typechecks.
-- (we'll have no applicable evaluation rules if we ask for a non-existent position).





Let's try proving that our nth definition is well-typed! (This is long/messy)


                                                                                                                   ---------------------------Ty-Var
                                                                                                                   {(xs,[Z])...}|-xs:[Z]
                                                                       ------------------------------------Ty-Var  ---------------------------Ty-head   ----------------Ty-Var  ----------Ty-Int
                                                                        {(self,[Z]->Z->Z)...}|-self:[Z]->Z->Z      {(xs,[Z])...}|-(tail xs):[Z]          {(n,Z)...}|-n:Z        {...}|-1:Z
------------TyVar ---------Ty-int ---------------------Ty-Var          ------------------------------------------------------------------------Ty-app   -----------------------------------Ty-Sub
{(n,Z)...}|-n:Z   {...}|-0:Z      {(xs,[Z])...}|-xs:[Z]                 {(self,[Z]->Z->Z),(xs,[Z])...}|-(self (tail xs)): Z->Z                           {(n,Z)...}|-(n-1): Z
-------------------------Ty-eq    ---------------------------Ty-head   --------------------------------------------------------------------------------------------------------------------Ty-app                        
{(n,Z)...}|- (n=0): B             {(xs,[Z])...}|- (head xs): Z          {(self,[Z]->Z->Z),(xs,[Z]),(n,Z)}|- ((self (tail xs)) (n-1)): Z
----------------------------------------------------------------------------------------------------------------------------------------------Ty-if
{(self,[Z]->Z->Z),(xs,[Z]),(n,Z)}|- if (n=0) (head xs) (self (tail xs) (n-1)):  Z
----------------------------------------------------------------------------------------------------------------Ty-λ
{(self,[Z]->Z->Z),(xs,[Z])}|- \n:Z. if (n=0) (head xs) (self (tail xs) (n-1)): Z->Z
----------------------------------------------------------------------------------------------------------------Ty-λ
{(self,[Z]->Z->Z)}|- (\xs:[Z]. \n:Z. if (n=0) (head xs) (self (tail xs) (n-1))): [Z]->(Z->Z)
----------------------------------------------------------------------------------------------------------------Ty-λ
{} |- (\self:[Z]->Z->Z. \xs:[Z]. \n:Z. if (n=0) (head xs) (self (tail xs) (n-1))) : ([Z]->Z->Z)->([Z]->(Z->Z))
----------------------------------------------------------------------------------------------------------------Ty-Fix
{} |- fix (\self:[Z]->Z->Z. \xs:[Z]. \n:Z. if (n=0) (head xs) (self (tail xs) (n-1))) : [Z]->Z->Z

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


⊢⟦ℤ𝔹⟧→

⟦ℤ⟧→⟦𝔹⟧→
Γ⊢λℤ→𝔹→
↦⟦⟧

→⊢↦Γλℤ𝔹⟦⟧⦅⦆ 

Γ⊢λℤ→𝔹→
↦
⟦⟧
⦅⦆