3

I am reading the article "Introduction to Type Theory" by Herman Geuvers, the chapter explaining the Fitch style of natural inference. I stuck at the exercise 1.3 (first two are simple):

Construct a term of type ((α→β)→α)→(α→α→β)→α

Only abstraction and application rules are allowed.

This math.stackexchange article suggest that to get a term of type α I should assume 

| x : (α→β)→α
|-----------------
|   | y: α→(α→β)
|   |-------------

I have no idea what next.

UPD:

The full answer is:

| x : (α→β)→α
|-----------------
|   | y : α→(α→β)
|   |-------------
|   |   | z : α
|   |   |-----------
|   |   | yz : α→β
|   |   | yzz : β
|   |   λz.yzz : α→β
|   |   x(λz.yzz) : α
|   λy.x(λz.yzz) : α→(α→β)→α
λx.λy.x(λz.yzz) : ((α→β)→α)→(α→(α→β))→α

Thank you Rob

Community
  • 1
amakarov
  • 177

1 Answers1

2

It may help to think of this as an exercise in (functional) programming. You want a function that maps a function $f$ of type $ (\alpha \rightarrow \beta) \rightarrow \alpha$ and a function $g$ of type $\alpha \rightarrow \alpha \rightarrow \beta$ to an element of type $\alpha$. To do this, the only promising approach is to apply $f$ to something and that something must have type $\alpha \rightarrow \beta$. But we can get something of that type using $g$, namely $\lambda x :\alpha \cdot g x x$. So the bottom line of the proof can be the following $\lambda$-expression: $$\lambda f : (\alpha \rightarrow \beta)\rightarrow \alpha\cdot\lambda g : \alpha \rightarrow \alpha \rightarrow \beta\cdot f(\lambda x :\alpha\cdot g x x)$$

Rob Arthan
  • 48,577