Find the lambda-terme without free variables of the following types?

Question

Could someone please explain the process of finding the lambda-terme without free variables of the following types ? I have some idea on how I should solve this but I'm not really sure it's the right way.

a) p->(q->q)
b) (p->q)->((q->r)->(p->r))
c) (p->(q->(q->r)))->(p->(q->r))

Answer 1

a) p -> (q -> q)

We need something to take a p,

\p -> …

and produce a q -> q, so we repeat, taking a q, and the only thing we can do is then return that q

\p -> \q -> q

we can add parens for emphasis:

\p -> (\q -> q)

b) (p -> q) -> ((q -> r) -> (p -> r))

We repeat. Our term starts by taking a function from p to q:

\p2q -> …

It must return a function of type ((q -> r) -> (p -> r)), so we start by returning something taking a function from q to r

\p2q -> \q2r -> …

And we now need it to produce an r given a p. There are only so many ways to piece together the available pieces:

\p2q -> \q2r -> \p -> q2r (p2q p)

Again, with parenthesis for emphasis:

\p2q -> (\q2r -> (\p -> q2r (p2q p)))

c) (p -> (q -> (q -> r))) -> (p -> (q -> r))

Hmm, my naming convention falls a little short on this one ;)

First, our term takes a (p -> (q -> (q -> r))):

\p2q2q2r -> …

Next, we must produce a term of type (p -> (q -> r)), so we let it take a p, and next take a q:

\p2q2q2r -> \p -> \q -> …

Producing an r now just involves piecing together what we have

\p2q2q2r -> \p -> \q -> ((p2q2q2r p) q) q

Hoped that helped with your homework ;)