Trouvez les types les plus généraux des termes de calcul lambda suivant

Question

Je ne parviens pas à comprendre pourquoi ce sont les types les plus généraux pour leurs chiffres de l'Église respectives:

2 = λf.λx. f (f x) : (α → α) → α → α 

1 = λf.λx. f x : (α → β) → α → β 

0 = λf.λx. x : β → α → α 

Je pensais que tous les chiffres de l'Église avaient le même type:

(α → α) → α → α 

aussi comment pourrais-je trouver un type général pour l'opérateur add

λm.λn.λf.λx. m f (n f x) 

Toute aide serait vraiment appréciée, merci!

Answer 1

Commençons par le chiffre Eglise zéro:

λf.λx. x : β → α → α 

En ne considérant que λf.λx. partie, on peut en déduire que nous avons une fonction à deux arguments, d'où son type est α → β → γ, où α et β position pour types d'arguments et γ représente le type de résultat. Maintenant, le corps x contraint encore le type: le type de retour de notre fonction doit être le même que celui de son second argument. Cela donne α → β → β, ou après le changement de nom (α ↔ β): λf.λx. x : β → α → α. C'est le type le plus général pour zéro, puisque nous n'avons pas utilisé le fait que f devrait être une fonction, en fait, l'Église zéro numéral dans non typé lambda calcul ne s'en soucie pas: il oublie juste son premier argument. Et puisque β est juste un espace réservé, vous pouvez spécialiser à α → α, ce qui se traduit par un type plus concret pour zéro - λf.λx. x : (α → α) → α → α.

Regardons 1:

λf.λx. f x : (α → β) → α → β 

Encore une fois, il est une fonction à deux arguments: α → β → γ, mais cette fois-ci (voir le corps de 1) nous savons que le premier argument f est une fonction, donc f a un certain type δ → ε, que nous devrions remplacer par α: (δ → ε) → β → γ. Maintenant, nous savons que nous devons être en mesure d'appliquer f-x, ce qui signifie que le type de x et le type d'argument de f doit être égal: δ = β, donc, nous avons atteint (β → ε) → β → γ. Mais ce n'est pas tout ce que nous savons, f x a le type ε, et notre nombre renvoie f x, en appliquant cette information, nous obtenons ε = γ. En intégrant tout cela, nous arrivons au (β → γ) → β → γ, ou après le renommage: λf.λx. f x : (α → β) → α → β. Encore une fois nous n'avons utilisé aucune information sur nos intentions d'utilisation, c'est pourquoi nous avons le type le plus général et, bien sûr, il peut être spécialisé (par la restriction β = α) à λf.λx. f x : (α → α) → α → α.

Il est 2 Tournons maintenant:

λf.λx. f (f x) : (α → α) → α → α 

Je ne vais pas répéter toutes les étapes cette fois-ci, mais (comme une étape intermédiaire) nous pouvons arriver à λf.λx. f (f x) : (α → β) → α → β.Notez cependant que cette fois-ci, le résultat de f est en lui-même: f (f x), ce qui signifie que les types d'entrée et de sortie de f doivent être égaux, donc β = α, et le type le plus général est cette fois λf.λx. f (f x) : (α → α) → α → α.

(*) Notez que Église 3, 4, etc. ont le même type le plus général que 2 faire, parce que les applications de fonctions multiples ne nous donnent aucune information supplémentaire pour se spécialiser davantage le caractère.

---

En ce qui concerne la fonction d'addition λm.λn.λf.λx. m f (n f x), laissez-moi être un peu plus laconique:

• Supposons que l'expression est de type α → β → γ → δ → ε.
• m est une fonction de 2 arguments: α doit être limitée à α' → α'' → α'''
• même pour n: β doit être restreint à β' → β'' → β'''
• m 's et n' premier argument a le même type, qui est la type de f: α' = β' = second type de l'argument de γ
• n est δ
• 'type de résultat s est égal à m' n secondes type d'argument s: β''' = α''
• Unissons toutes les connaissances ci-dessus pour n : γ → δ → α''
• Même chose pour m : γ → α'' → ε
• Par conséquent, le type de résultat est (γ → α'' → ε) → (γ → δ → α'') → γ → δ → ε

Renommons les variables pour les rendre plus jolies:

le type le plus général pour λm.λn.λf.λx. m f (n f x) est

(β → γ → ε) → (β → α → γ) → β → α → ε.

Vérifions qu'il peut être spécialisé à ce qu'on pourrait attendre d'être une opération binaire sur les chiffres de l'Église (β = α → α, γ = α, ε = α):

((α → α) → α → α) → ((α → α) → α → α) → (α → α) → α → α.