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

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

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

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

1 ответ

  1. Я предполагаю, что вы говорите о просто типизированном лямбда-исчислении, расширенном типами intданных booleanи_≤_, терминами 12и правилами вывода типов

    --------------------------------
    Γ ⊢ _≤_ : 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 ∎