arbres pour preuve lambda-calcul simplement typé

Question

je dois indiquer le type du terme

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

et prouver à l'aide d'un arbre de preuve. Je suis assez certain que cela prend 2 comme une entrée pour x, puis en comparant 2 à 1 et en renvoyant un boolean. Cela signifie que le type du terme serait int → boolean. Je ne suis pas sûr de savoir comment écrire un arbre de preuve pour cela. Si quelqu'un pouvait me montrer quelques exemples ou expliquer comment faire un problème similaire, ce serait génial.

Answer 1

Je suppose que vous parlez du lambda-calcul simplement typé étendu avec les types de données int et boolean, les termes _≤_, 1 et 2, et les règles de dérivation de frappe

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

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

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

utilisant, et la norme STLC règles de typage, le type de votre terme est pasint → boolean, plutôt, il est boolean comme nous le verrons ci-dessous. En outre, il β-réduit à 2 ≤ 1, donc cela devrait vous montrer assez facilement que c'est un boolean.

Mais maintenant, à la viande de celui-ci: l'arbre de dérivation de frappe:

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

Pour économiser de l'espace horizontal, nous allons faire le reste dans un nouvel arbre:

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