lambda-calculus - 简单类型 lambda 演算的证明树

Question

我需要说明术语的类型

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

并使用证明树证明它。我相当确定这是将 2 作为 的输入x，然后将 2 与 1 进行比较并返回 a boolean。这意味着术语的类型是int → boolean。我只是不确定如何为其编写证明树。如果有人可以向我指出一些示例或解释如何解决类似的问题，那就太好了。

Answer 1

我假设您谈论的是简单类型的 lambda 演算，它扩展了数据类型int和boolean、术语_≤_、1和2，以及类型推导规则

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

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

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

使用这些以及标准的 STLC 输入规则，您的术语的类型不是 int → boolean，而是boolean我们将在下面看到的。此外，它 β-减少到2 ≤ 1，因此应该很容易告诉您它是boolean。

但现在是它的核心：类型派生树：

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

为了节省水平空间，让我们在新树中完成剩下的工作：

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