Proof Bäume für einfach typisierten Lambda-Kalkül

Question

Ich brauche die Art des Begriffs

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

und beweisen, dass es mit einem Beweisbaum zu erklären. Ich bin ziemlich sicher, dass dies 2 als Eingabe für x, dann Vergleich 2 zu 1 und eine boolean zurückgibt. Dies bedeutet, dass die Art des Begriffs int → boolean wäre. Ich bin mir einfach nicht sicher, wie ich einen Beweisbaum dafür schreiben soll. Wenn jemand mich auf einige Beispiele hinweisen oder erklären könnte, wie man ein ähnliches Problem macht, wäre das großartig.

Answer 1

Ich nehme an, Sie sprechen über die einfach typisierten Lambda-Kalkül mit den Datentypen erweitert int und boolean, wobei die Begriffe _≤_, 1 und 2 und die Typisierung Ableitungsregeln

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

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

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

diese verwenden, und die Standard-STLC Tippregeln, der Typ Ihrer Amtszeit ist nichtint → boolean, eher ist es boolean wie wir unten sehen werden. Auch es reduziert sich auf 2 ≤ 1, so dass Sie ziemlich leicht zeigen sollten, dass es sich um eine boolean handelt.

Aber jetzt, um das Fleisch davon: die Typisierung Herleitungsbaum:

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

auf horizontalen Raum zu sparen, lassen Sie sich in einem neuen Baum den Rest:

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