Preuve de confluence pour un système de réécriture simple

14

Supposons que nous ayons un langage simple composé des termes:

  • true
  • false
  • si sont des termes, alorst1,t2,t3ift1thent2elset3

Supposons maintenant les règles d'évaluation logiques suivantes:

iftruethent2elset3t2[E-IfTrue]iffalsethent2elset3t3[E-IfFalse]t1t1ift1thent2elset3ift1thent2elset3[E-If]

Supposons que nous ajoutions également la règle géniale suivante:

t2t2ift1thent2elset3ift1thent2elset3[E-IfFunny]

Pour ce langage simple avec les règles d'évaluation données, je souhaite prouver ce qui suit:

Théorème: Si et alors il existe un terme tel que et .rsrtusutu

Je le prouve par induction sur la structure de . Voici ma preuve jusqu'à présent, tout a bien fonctionné, mais je suis coincé dans le tout dernier cas. Il semble que l'induction sur la structure de ne soit pas suffisante, quelqu'un peut-il m'aider?rr

Preuve. Par induction sur , on séparera toutes les formes que peut prendre:rr

  1. r est une constante, rien à prouver puisqu'une forme normale n'évalue rien.
  2. r= si vrai alors sinon . (a) les deux dérivations ont été effectuées avec la règle E-IfTrue. Dans ce cas , il n'y a donc rien à prouver. (b) une dérivation a été effectuée avec la règle E-IfTrue, l'autre avec la règle E-Funny. Supposons que été fait avec E-IfTrue, l'autre cas est prouvé de manière équivalente. Nous savons maintenant que . On sait aussi que si vrai alorsr2r3s=trss=r2t=r2 sinon et qu'il existe une dérivation r 2r 2 (la prémisse). Si nous choisissons maintenant u = r r3r2r2 , nous concluons l'affaire.u=r2
  3. si faux alors r 2 sinon r 3 . Prouvé de manière équivalente comme ci-dessus.r=r2r3
  4. sialorssinonavecvrai ou faux. (a) les deux dérivations ont été effectuées avec la règle E-If. On sait maintenant quesipuissinonetsipuissinon. On sait également qu'il existe des dérivationset(les prémisses). On peut maintenant utiliser l'hypothèse d'induction pour dire qu'il existe un termetel quer=r1r2r3r1s=r1r2r3t=r1r2r3r1r1r1r1r1r1r1et . Nous concluons maintenant le cas en disant if puis else et en notant que et par la règle E-If. (b) une dérivation a été effectuée par la règle E-If et une par la règle E-Funny.r1r1u=r1r2r3sutu

Ce dernier cas, où une dérivation a été faite par E-If et une par E-Funny est le cas qui me manque ... Je n'arrive pas à pouvoir utiliser les hypothèses.

L'aide sera très appréciée.

codd
la source
@Gilles extrêmement bien fait avec le montage. Je ne savais pas que le moteur TeX de SE était capable de tout cela ... :-)
codé le
Ai-je tort ou cet exercice est tiré de Pierce "Types et langages de programmation"?
Fabio F.
@FabioF. C'est en effet du livre Pierce's Types and Programming Languages. Il fournit une preuve que je trouve peu claire, en raison de la façon dont il effectue l'induction. C'est pourquoi j'ai essayé de le prouver moi-même par induction sur la structure. Je pensais mentionner que cela venait du livre, mais je pensais que ce serait plutôt hors de propos. Bien remarqué cependant!
codd

Réponses:

7

Bon, considérons donc le cas où , s a été dérivé en appliquant la règle E-If et t a été dérivé en appliquant la règle E-Funny: So s = i fr=ift1thent2elset3st t 1t 1 et t = i fs=ift1thent2elset3t1t1 t 2t 2 .t=ift1thent2elset3t2t2

L' que nous recherchons est u = i fu . s u découle de la règle E-Funny et t u découle de la règle E-If.u=ift1thent2elset3sutu

sepp2k
la source
Battez-moi. Bon travail.
Patrick87
Mon Dieu, je regardais vraiment trop loin ... Merci!
codd
Vous les avez mélangés cependant, suit de E-Funny. Ou est-ce que je vois quelque chose de mal? su
codd
@Jeroen Vous avez raison - je les ai mélangés. Fixé maintenant.
sepp2k
8

Un peu de terminologie peut vous aider si vous voulez chercher: ces règles sont des règles de réécriture , elles n'ont rien à voir avec les systèmes de types¹. La propriété que vous essayez de prouver s'appelle confluence ; plus précisément, c'est une forte confluence : si un terme peut être réduit de différentes manières à une étape, il peut converger à l'étape suivante. En général, la confluence permet qu'il y ait un nombre quelconque d'étapes et pas une seule: si et r t alors il y a u tel que s u et t ursrtusutu - si un terme peut être réduit de différentes manières, quelle que soit la distance à laquelle il a divergé, il peut éventuellement revenir en arrière.

La meilleure façon de prouver une propriété de ces règles de réécriture définies par induction est par induction sur la structure de la dérivation de la réduction, plutôt que sur la structure du terme réduit. Ici, l'un ou l'autre fonctionne, car les règles suivent la structure du terme de gauche, mais le raisonnement sur les règles est plus simple. Au lieu de plonger dans le terme, vous prenez toutes les paires de règles et voyez quel terme pourrait être un côté gauche pour les deux. Dans cet exemple, vous obtiendrez les mêmes cas à la fin, mais un peu plus vite.

Dans le cas qui vous pose problème, un côté réduit la partie «si» et l'autre côté réduit la partie «alors». Il n'y a pas de chevauchement entre les deux parties qui changent ( dans [E-If], t 2 dans [E-IfFunny]), et il n'y a pas de contrainte sur t 2 dans [E-If] ou sur t 1 dans [E- IfFunny]. Donc, quand vous avez un terme auquel les deux règles s'appliquent - qui doit être de la forme i ft1t2t2t1 , vous pouvez choisir d'appliquer les règles dans l'un ou l'autre ordre:ifr1thenr2elser3

ifr1thenr2elser3[E-If][E-IfFunny]ifr1thenr2elser3ifr1thenr2elser3[E-IfFunny][E-If]ifr1thenr2elser3

¹ Vous verrez parfois des types et des réécritures ensemble, mais à la base ce sont des concepts orthogonaux.

Gilles 'SO- arrête d'être méchant'
la source