Proof деревья для простого типизированного лямбда-исчисления

Question

мне нужно указать тип термина

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

и доказать это, используя дерево доказательства. Я вполне уверен, что это занимает 2 в качестве ввода для x, а затем сравнение 2 к 1 и возврат boolean. Это означает, что тип этого термина будет int → boolean. Я просто не знаю, как написать для него дерево доказательств. Если кто-то может указать мне на некоторые примеры или объяснить, как сделать подобную проблему, это было бы здорово.

Answer 1

Я полагаю, вы говорите о просто типизированного лямбда-исчисления расширенной с типами данных 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 ∎