example1.txt

Homework 1

# one can write arbitrary comments in this file after hashes

constants of type e : a b-d
constants of type <e,t> : P Q; display as: one-place predicate
constants of type <e*e,t> : R; display as: two-place predicate
variables of type e : x-z
variables of type <et> : X Y; display as: one-place predicate

exercise semantic types
title Semantic Types
directions Give the semantic type of the following lambda-expressions. You may want to simplify them in your mind if necessary before assigning a type.
points per exercise 20

Lx[P(x) & Q(x)]

exercise lambda conversion
title Lambda Conversion
directions After checking that the type of the function and the type of the
directions argument(s) match, simplify the following expressions performing
directions one lambda-conversion at a time.
points per exercise 10

[Lx.P(x) & Q(x)] (a)
[LxLy.R(a,y) & Q(x)] (a) (b)
[Lx.Ey[R(y,x)]] (y)
[Lx.a] (b)
[Lx.P(x) -> Ex.R(x,b)] (a)
[LxLx.P(x) -> R(x,c)] (a) (b)