Proof trees for simply typed lambda calculus

Question

I need to state the type of the term

((λx : int. (x ≤ 1)) 2)

and prove it using a proof tree. I'm fairly certain that this is taking 2 as an input for x, then comparing 2 to 1 and returning a boolean. This means the type of the term would be int → boolean. I'm just not sure how to write a proof tree for it. If someone could point me towards some examples or explain how to do a similar problem that would be great.

Cactus Cactus · Accepted Answer · 2016-11-04T08:22:20

I assume you are talking about the simply typed lambda calculus extended with the datatypes int and boolean, the terms _≤_, 1 and 2, and the typing derivation rules

--------------------------------
Γ ⊢ _≤_ : int → int → boolean

------------
Γ ⊢ 1 : int 

------------                
Γ ⊢ 2 : int

Using these, and the standard STLC typing rules, the type of your term is not int → boolean, rather, it is boolean as we will see below. Also, it β-reduces to 2 ≤ 1, so that should show you quite easily that it is a boolean.

But now to the meat of it: the typing derivation tree:

{x : int} ⊢ _≤_ : int → int → boolean       {x : int} ⊢ x : int             
----------------------------------------------------------------
                     {x : int} ⊢ x ≤_ : int → boolean                 {x: int} ⊢ 1 : int
                     --------------------------------------------------------------------
                                      {x: int} ⊢ x ≤ 1 : boolean

To save on horizontal space, let's do the rest in a new tree:

{x: int} ⊢ x ≤ 1 : boolean
----------------------------------------
{} ⊢ (λx : int. (x ≤ 1) : int → boolean               {} ⊢ 2 : int
-------------------------------------------------------------------
                 {} ⊢ ((λx : int. (x ≤ 1)) 2) : boolean ∎

Proof trees for simply typed lambda calculus

1 Answers