CS 463
Homework 2 Solution
Spring 2024


§ 1 – Evaluating Terms

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

1.1

   ( (λn . n – 3)  8)
⟹ E-App-Abs
   8-3
⟹ E-Sub
   5

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

1.2

   ( (λa.a+1) (2+3) )
⟹ E-App2 (via E-Add)
   ((λa.a+1) 5)
⟹ E-App-Abs
   5+1
⟹ E-Add
   6

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

1.3

   ( ( (λx. (λy. if (x=y) x 0) ) (1+4)) (2*3))
⟹ E-App1 (via E-App2, E-Add)
   ( ( (λx. (λy. if (x=y) x 0) ) 5) (2*3))
⟹ E-App1 (via E-App-Abs)
   ((λy. if (5=y) 5 0) (2*3))
⟹ E-App2 (via E-Mul)
   ((λy. if (5=y) 5 0) 6)
⟹ E-App-Abs
   if (5=6) 5 0
⟹ E-If (via E-Eq)
   if false 5 0
⟹ E-If-false
   0

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

1.4

   (((λf. λn. (f n)) (λx.4*x)) 7)
⟹ E-App1 (via E-App-Abs)
   ((λn. ((λx.4*x) n)) 7)
⟹ E-App-Abs
   ((λx.4*x) 7)
⟹ E-App-Abs
   4*7
⟹ E-Mul
    28

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

1.5

   ((λxs. cons 3 xs) (if false (cons 2 nil) nil))
⟹ E-App2 (via E-If-false)
   ((λxs. cons 3 xs) nil)
⟹ E-App-Abs
   cons 3 nil


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

1.6 (extra credit +1):

    ((λg.(λx.g x)) (λh.h))
 ==> E-App-Abs                (substitute (λh.h) into λg)
    λx.((λh.h) x)             (and that's already a value in our language)

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

§ 2 – Encodings

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

2.1

   (not false)
⟹ expand def'n of not
   ((λa. (a false) true) false)
⟹ E-App-Abs
   ((false false) true)
⟹ expand def'n of false
   ((λx. (λy. y)) false) true)
⟹ E-App1 (via E-App-Abs)
   ((λy.y) true)
⟹ E-App-Abs
   true

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

2.2

   ((or true) false)
⟹ expand def'n of or
   (((λa. λb. ((a a) b)) true) false)
⟹ E-App1 (via E-App-Abs)
   (  (λb.((true true) b)) false)
⟹ E-App-Abs
   ((true true) false)
⟹ expand def'n true
   (((λx. λy. x) true) false)
⟹ E-App1 (via E-App-Abs) 
   ((λy.true) false)
⟹ E-App-Abs
   true

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

2.3

   ((and true) false)
⟹ expand def'n and
   (((λa. λb. ((a b) a)) true) false)
⟹ E-App1 (via E-App-Abs)
   ((λb. ((true b) true)) false)
⟹ E-App-Abs
   ((true false) true)
⟹ expand def'n true
   (((λx. λy.x) false) true)
⟹ E-App1 (via E-App-Abs)
   ((λy.false) true)
⟹ E-App-Abs
   false

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

2.4

nand = λx. λy. ((x  (not y)) true)          (this is one possible solution)

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

2.5

   ((nand true) false)
⟹ expand def'n of nand                       (your solution might diverge here!)
   (((λx. λy. ((x (not y)) true)) true) false)
⟹ E-App1 (via E-App-Abs)                              (x ↦ true )
   ((λy. ((true (not y)) true)) false)
⟹ E-App-Abs                                           (y ↦ false)
   ((true (not false)) true)
⟹ expand def'n of true
   (((λx.λy.x) (not false)) true)
⟹ expand def'n of not
   (((λx.λy.x) ((λa. (a false) true) false)) true)
⟹ E-App1 (via E-App2, E-App-Abs)                      (a ↦ false)
   (((λx.λy.x) ((false false) true)) true)
⟹ expand false
   (((λx.λy.x) (((λx.λy.y) false) true)) true)
⟹ E-App1 (via E-App2, E-App1, E-App-Abs)              (x ↦ false)
   (((λx.λy.x) ((λy.y) true)) true)
⟹ E-App1 (via E-App2, E-App-Abs)                      (y ↦ true )
   (((λx.λy.x) true) true)
⟹ E-App1 (via E-App-Abs)                              (x ↦ true )
   ((λy.true) true)
⟹ E-App-Abs                                           (y ↦ true )
   true

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

§ 3 – Extending the Language

t ::= x | λx.t | (t t) | true | false | if t t t | ~t | t = t
    | <#> | t + t | t-t | t*t | t<t | t>t
    | nil | cons t t | isnil t | head t | tail t
    | fix t 
    | optional t | empty | orelse t t | ispresent t | get t
v ::= λx.t | true | false | <#> | nil | cons t t | fix t | present t | empty


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

Defining evaluation rules.


           t1 -> t1'
--------------------------------   E-orelse-1
orelse t1 t2  ->  orelse t1' t2


--------------------------------   E-orelse-optional
orelse (optional t1) t2  ->  t1


----------------------             E-orelse-empty
orelse empty t2 -> t2


    t -> t'
----------------                   E-get-1
get t -> get t'


----------------------             E-get-optional
get (optional t) -> t


          t  ->  t'
-----------------------------      E-ispresent-1
ispresent t  ->  ispresent t'


--------------------------------   E-present-optional
ispresent (optional t)  ->  true


--------------------------         E-ispresent-empty
ispresent empty  ->  false


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

3.2 

more = λx. λoy. x + (orelse oy 0)
more = λx. λoy. x + (if (ispresent oy) (get oy) 0)

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

3.3

isbig = λon. if (ispresent on) (optional ((get on)>1000)) empty

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

§ 4 – Extra Credit

addAnyPresent = fix (λself.
                       λxs. if (isnil xs)
                               0
                               (if (ispresent (head xs))
                                   ((get (head xs)) + (self (tail xs)))
                                   (self (tail xs))
                    )          )


addAnyPresent = fix (λself.
                       λxs. if (isnil xs)
                               0
                               ((orelse (head xs) 0) + (self (tail xs)))
                    )          )

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