Quel est l'intérêt de la conversion

Je pense que je ne le comprends pas, mais -conversion me semble être une -conversion qui ne fait rien, un cas particulier de -conversion où le résultat n'est que le terme dans l'abstraction lambda car il n'y a rien à faire, une sorte de conversion inutile.β β $\eta$$\beta$$\beta$$\beta$

Alors peut-être que -conversion est quelque chose de vraiment profond et différent de cela, mais si c'est le cas, je ne comprends pas et j'espère que vous pourrez m'aider.$\eta$

(Merci et désolé, je sais que cela fait partie des bases du calcul lambda)

Mise à jour [2011-09-20]: J'ai développé le paragraphe sur l' expansion $\eta$ et l'extensionnalité. Merci à Anton Salikhmetov d'avoir signalé une bonne référence.

$\eta$ -conversion$(\lambda x . f x) = f$ est un cas spécial deconversion$\beta$ -uniquementdans le cas spécial lorsque$f$ est lui-même une abstraction, par exemple, si$f = \lambda y . y y$ alors

$$(\lambda x . f x) = (\lambda x . (\lambda y . y y) x) =_\beta (\lambda x . x x) =_\alpha f.$$ Mais que faire si$f$ est une variable ou une application qui ne se réduit pas à une abstraction?

D'une certaine manière, la règle $\eta$ est comme un type particulier d'extensionnalité, mais nous devons faire un peu attention à la façon dont cela est énoncé. Nous pouvons affirmer l'extensionnalité comme:

1. pour tous les $\lambda$ -terms $M$ et $N$ , si $M x = N x$ alors $M = N$ , ou
2. pour tout si ∀ x . f x = g x puis f = g .$f, g$$\forall x . f x = g x$$f = g$

Le premier est une méta-déclaration sur les termes du -calculus. En lui, x apparaît comme une variable formelle, c'est-à-dire qu'il fait partie du λ -calculus. On peut le prouver à partir des règles β η , voir par exemple le théorème 2.1.29 dans "Lambda Calculus: its Syntax and Semantics" de Barendregt (1985). Il peut être compris comme un énoncé de toutes les fonctions définissables , c'est-à-dire celles qui sont des dénotations de termes λ .$\lambda$$x$$\lambda$$\beta\eta$$\lambda$

La deuxième affirmation est la façon dont les mathématiciens comprennent généralement les énoncés mathématiques. La théorie du -calcul décrit un certain type de structures, appelons-les " λ -models ". Un modèle λ peut être indénombrable, il n'y a donc aucune garantie que chaque élément de celui-ci correspond à un terme λ (tout comme il y a plus de nombres réels que d'expressions décrivant des réels). L'extensionnalité dit alors: si nous prenons deux choses f et g dans un modèle λ , si f x = g x pour tout x dans le modèle, alors f = $\lambda$$\lambda$$\lambda$$\lambda$$f$$g$$\lambda$$f x = g x$$x$$f = g$. Or, même si le modèle satisfait la règle , il n'a pas besoin de satisfaire l'extensionnalité dans ce sens. (Référence nécessaire ici, et je pense que nous devons faire attention à la façon dont l'égalité est interprétée.)$\eta$

Il existe plusieurs façons de motiver conversions β - et η . Je choisirai au hasard la catégorie théorique, déguisée en λ -calculus, et quelqu'un d'autre peut expliquer d'autres raisons.$\beta$$\eta$$\lambda$

Considérons le -calculus typé (car il est moins déroutant, mais plus ou moins le même raisonnement fonctionne pour le λ -calculus non typé ). L' une des lois fondamentales qui devraient est la loi détient exponentielle C A × B ≅ ( C B ) A . (J'utilise les notations A → B et B A de manière interchangeable, en sélectionnant celle qui semble meilleure.) Que font les isomorphismes i : C A × B → ( C B ) A et j $\lambda$$\lambda$

$$C^{A \times B} \cong (C^B)^A.$$ $A \to B$$B^A$$i : C^{A \times B} \to (C^B)^A$ ressemble à, écrit en λ -calculus? On peut supposer qu'ils seraient i = λ f : C A × B . λ a : A . λ b : B . f ⟨ a , b ⟩ et J = λ g : ( C B ) A . λ p : A × $j : (C^B)^A \to C^{A \times B}$$\lambda$ $$i = \lambda f : C^{A \times B} . \lambda a : A . \lambda b : B . f \langle a, b \rangle$$ Un calculcourte avec un couple de ß -réductions (y compris le β -réductions π 1 ⟨ un , b ⟩ = a et π 2 ⟨ un , b ⟩ = b pourproduits) nous apprend que, pour chaque g : ( C B ) A nous avons i ( j g ) $$j = \lambda g : (C^B)^A . \lambda p : A \times B . g (\pi_1 p) (\pi_2 p).$$ $\beta$$\beta$$\pi_1 \langle a, b \rangle = a$$\pi_2 \langle a, b \rangle = b$$g : (C^B)^A$ Puisque i et j sont inversesdeautre, nous nous attendons à i ( j g ) = g , mais pour prouver effectivement cenous devons utiliser η -réduction deux fois: i ( j g ) = ( λ a : A . Λ b : B . g a b ) = η $$i (j g) = \lambda a : A . \lambda b : B . g a b.$$ $i$$j$$i (j g) = g$$\eta$ C'est donc une des raisons pour avoir desréductions η . Exercice: quellerègle η est nécessaire pour montrer que j ( i f ) = f ? $$i(j g) = (\lambda a : A . \lambda b : B . g a b) =_\eta (\lambda a : A . g a) =_\eta g.$$ $\eta$$\eta$$j (i f) = f$

Afin de répondre à cette question, nous pouvons fournir la citation suivante de la monographie correspondante «Lambda Calculus. Sa syntaxe et sa sémantique »(Barendregt, 1981):

$\beta\eta$$\lambda$$\lambda + \text{ext}$$\text{ext}$$M x = N x \Rightarrow M = N$

$M =_{\beta\eta} N \Leftrightarrow \lambda\eta \vdash M = N \Leftrightarrow \lambda + \text{ext} \vdash M = N$

[Sa preuve est basée sur le théorème suivant.]

$\lambda + \text{ext}$$\lambda\eta$$(\text{ext}) \Rightarrow (\eta)$

$\lambda\eta$

$M$$N$$\lambda\eta \vdash M = N$$\lambda\eta + M = N$

Les théories HP-complètes [d'après Hilbert-Post] correspondent aux théories cohérentes maximales en théorie des modèles pour la logique du premier ordre.

$\lambda$$\beta$$\eta$

• $\lambda x y.x$$\lambda x y.y$ $\beta\eta$$\beta\eta$

• $\iota$
  

  1. $u\ =_\iota\ v \Rightarrow t\ u\ =_\iota\ t\ v$

  2. $\beta\eta$$t$$u$$t=_\iota u$$t\neq_{\beta\eta}u$

$t$$u$$t=_{\beta\eta\iota}u$

Ceci est une conséquence du théorème de Böhm.

$\eta$

$=_{\beta \eta}$$\rightarrow_{\beta\eta}$$M=N$$\lambda x.M = \lambda x.N$$=_{\beta}$

$=_{\beta}$$=_{\beta\eta}$$\lambda x. Mx = M$$Mx=Nx$$M=N$