Calcul lambda: différence entre les contextes et les contextes d'évaluation

Tout d'abord, je voudrais dire que mon texte ci-dessous peut contenir des erreurs, alors n'hésitez pas à signaler toute erreur dans ma formulation de la question.

Considérons un calcul lambda non typé avec des booléens et des instructions if dont les termes sont donnés par cette syntaxe:

 t ::= v | t t | if t t t | x
 v ::= \x.t | #t | #f

Les contextes C dans ce cas seraient donnés selon cette syntaxe:

C ::= [-] | \x. C | C t | t C | if C t t | if t C t | if t t C 

De plus, on pourrait définir des contextes d'évaluation E selon cette autre syntaxe:

E ::= [-] | \x. E | v E | E t | if E t t 

J'ai divisé ma question en trois sous-points que j'aimerais aborder.

1. Quand les deux notions sont-elles utilisées? Je sais par exemple que les contextes d'évaluation sont utilisés pour définir la sémantique du calcul, mais l'utilisation des contextes m'échappe encore quelque peu. J'aimerais aussi une confirmation de mes connaissances ici.
2. Quand doit-on préférer l'un à l'autre et pourquoi?
3. Pourriez-vous indiquer des articles pertinents qui pourraient m'aider à régler ce problème?

Le contexte est utilisé à de nombreuses fins, mais généralement pour définir des congruences sur les programmes. Les contextes d'évaluation sont un sous-ensemble de contextes. Ils sont généralement utilisés pour définir les relations de réduction. Permettez-moi de donner un exemple de chacun.

Une façon formelle de définir l'égalité des programmes consiste à dire que deux programmes et sont contextuellement égaux, ils peuvent se remplacer dans chaque contexte sans changement de comportement. Nous pouvons définir ceci comme suit: et sont contextuellement égaux pour tous les contextes de fermeture pour et : si et seulement si . Nous disons qu'un contexte se ferme pour si ni ni n'ont de variables libres. L'expressionN M N C [ ⋅ ] M N C [ M ] ⇓ t C [ N ] ⇓ t M , N C [ M ] C [ N ] M ⇓ t M $M$$N$$M$$N$$C[\cdot]$$M$$N$$C[M] \Downarrow t$$C[N] \Downarrow t$$M, N$$C[M]$$C[N]$$M \Downarrow t$signifie que le programme réduit en un nombre fini d'étapes à la valeur . (En passant, notez que la définition de l'équivalence contextuelle est plus impliquée pour les notions riches de calcul, par exemple les processus concurrents.)$M$$t$

En revanche, les contextes d'évaluation sont des contextes qui ne bloquent pas l'évaluation. Plus précisément, un contexte d'évaluation est un terme avec un trou au point où la prochaine étape de réduction atomique doit avoir lieu (ou peut avoir lieu pour un calcul non déterministe). La règle suivante devrait donc s'appliquer aux contextes d'évaluation: À titre d'exemple d'utilisation de contextes d'évaluation, considérons les règles de réduction pour lecalculpar valeur-appelλ-calcul, où nous ne réduisons pas sousλ. Donc, même lorsqueM→N, nous n'avons pas de réductionλx. M→λx. N. Cela peut facilement être exprimé avec la règle contextuelle générale ci-dessus, ainsi qu'une grammaire pour les contextes d'évaluation qui omet lesexpressionsλ. Les contextes d'évaluation ont d'abord été utilisés dans

$$\frac{M \rightarrow N}{E[M] \rightarrow E[N]}$$ $\lambda$$\lambda$$M \rightarrow N$$\lambda x.M \rightarrow \lambda x.N$$\lambda$Le rapport révisé sur les théories syntaxiques du contrôle séquentiel et de l'état par Felleisen et Hieb.

Un contexte est une notion syntaxique. Un contexte est un terme avec un trou dedans. (Parfois, il existe des contextes multi-trous, la définition sera donnée clairement dans ce cas.) La syntaxe des contextes est définie en prenant la syntaxe des termes et en permettant à un sous-terme d'être un trou au lieu d'un terme. En BNF (j'utilise le lambda-calcul comme un exemple, sans booléens et si des déclarations qui n'apportent rien à l'exemple.): C : : = [ ] | x | $[]$

$$C ::= [] \mid x \mid t \, C \mid C \, t \mid \lambda x.C$$

$C[]$$t$$C[t]$$t$$[]$$C[t]$$[]$$t$

$$(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}$$ $M \{x\leftarrow N\}$$x \mapsto N$$M$

$t$$M$$N$$x$$t = (\lambda x. M) \, N$$t$$t'$$t' = (\lambda x. M) \, N$$t$$C$$M$$N$$x$$t = C[(\lambda x. M) \, N]$$C[M \{x\leftarrow N\}]$

$$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \qquad \dfrac{M \to_\beta N}{C[M] \to_\beta C[N]} (\gamma)$$ $$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_\beta N}{\lambda x. M \to_\beta \lambda x. N} (C_\lambda) \qquad \dfrac{M \to_\beta N}{M \, P \to_\beta N \, P} (C_{@\lt}) \qquad \dfrac{M \to_\beta N}{P \, M \to_\beta P \, N} (C_{@\gt})$$

$$D ::= [] \mid x \mid t \, D \mid D \, t$$ $$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} \qquad \dfrac{M \to_{np} N}{D[M] \to_{np} D[N]}$$ $$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_{np} N}{M \, P \to_{np} N \, P} (C_{@\lt}) \qquad \dfrac{M \to_{np} N}{P \, M \to_{np} P \, N} (C_{@\gt})$$ $D$

$V$

$$V ::= x V_1 \ldots V_n \mid \lambda x. M$$ $$E ::= [] \mid M \, E \mid E \, V$$ $D$ $$\dfrac{}{(\lambda x. M) \, V \to_{cbva} M \{x\leftarrow V\}} (\beta_{cbva}) \qquad \dfrac{M \to_\beta N}{E[M] \to_{cbva} E[N]} (\gamma_{cbva})$$