Dowód konfluencji dla prostego systemu przepisywania

Załóżmy, że mamy prosty język, który składa się z terminów:

$\mathtt{true}$
$\mathtt{false}$
jeśli są warunkami, to podobnie jest z $t_1,t_2,t_3$ $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$

Załóżmy teraz następujące logiczne reguły oceny:

\begin{matrix} \frac{}{i f t r u e t h e n t_{2} e l s e t_{3} \to t_{2}} [E-IfTrue] \frac{}{i f f a l s e t h e n t_{2} e l s e t_{3} \to t_{3}} [E-IfFalse] \\ \frac{t_{1} \to t_{1}^{'}}{i f t_{1} t h e n t_{2} e l s e t_{3} \to i f t_{1}^{'} t h e n t_{2} e l s e t_{3}} [E-If] \end{matrix}

$\begin{gather*} \dfrac{} {\mathtt{if}\: \mathtt{true} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_2} \text{[E-IfTrue]} \quad \dfrac{} {\mathtt{if}\: \mathtt{false} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_3} \text{[E-IfFalse]} \\ \dfrac{t_1 \to t_1'} {\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1' \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3} \text{[E-If]} \\ \end{gather*}$

Załóżmy, że dodajemy również następującą funky zasadę:

\frac{t_{2} \to t_{2}^{'}}{i f t_{1} t h e n t_{2} e l s e t_{3} \to i f t_{1} t h e n t_{2}^{'} e l s e t_{3}} [E-IfFunny]

$\dfrac{t_2 \to t_2'} {\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1 \:\mathtt{then}\: t_2' \:\mathtt{else}\: t_3} \text{[E-IfFunny]}$

Dla tego prostego języka z podanymi zasadami oceny chcę udowodnić, co następuje:

Twierdzenie: Jeśli i to istnieje pewien termin taki, że i . $r \rightarrow s$ $r \rightarrow t$ $u$ $s \rightarrow u$ $t \rightarrow u$

Udowadniam to przez indukcję na strukturze . Oto mój dowód, jak dotąd, wszystko poszło dobrze, ale utknąłem w ostatniej sprawie. Wydaje się, że indukcja struktury nie jest wystarczająca, czy ktoś może mi pomóc? $r$ $r$

Dowód. Indukując na , rozdzielimy wszystkie formy, które może przyjąć: $r$ $r$

$r$ jest stałą, nic do udowodnienia, ponieważ normalna postać niczego nie ocenia.
$r=$ jeśli prawda, to inaczej . (a) oba pochodne wykonano zgodnie z zasadą E-IfTrue. W tym przypadku , więc nie ma nic do udowodnienia. (b) jedna pochodna została wykonana z zasadą E-IfTrue, a druga z zasadą E-Funny. Załóżmy, że zostało wykonane za pomocą E-IfTrue, drugi przypadek jest równoważnie udowodniony. Wiemy teraz, że . Wiemy również, że jeśli prawda, to inaczej i że istnieje pewna pochodna (przesłanka). Jeśli teraz wybierzemy , zakończymy sprawę. $r_2$ $r_3$ $s=t$ $r \rightarrow s$ $s = r_2$ $t =$ $r'_2$ $r_3$ $r_2 \rightarrow r'_2$ $u = r'_2$
$r=$ jeśli fałsz, to inaczej . Równie udowodnione jak wyżej. $r_2$ $r_3$
$r=$ jeśli to inaczej z true lub false. (a) oba wyprowadzenia wykonano zgodnie z zasadą E-If. Teraz wiemy, że jeśli następnie inny i jeśli następnie inny . Wiemy również, że istnieją i (przesłanki). Możemy teraz użyć hipotezy indukcyjnej, aby powiedzieć, że istnieje jakiś termin taki, że $r_1$ $r_2$ $r_3$ $r_1 \neq$ $s =$ $r'_1$ $r_2$ $r_3$ $t =$ $r''_1$ $r_2$ $r_3$ $r_1 \rightarrow r'_1$ $r_1 \rightarrow r''_1$ $r'''_1$ $r'_1 \rightarrow r'''_1$ i . Mamy teraz zakończyć sprawę mówiąc, jeśli następnie inny i zauważyć, że i przez E-IF reguły. (b) jedno wyprowadzenie zostało wykonane według zasady E-If, a drugie według zasady E-Funny. $r''_1 \rightarrow r'''_1$ $u =$ $r'''_1$ $r_2$ $r_3$ $s \rightarrow u$ $t \rightarrow u$

Ten drugi przypadek, w którym jedno wyprowadzenie zostało wykonane przez E-If, a drugie przez E-Funny, to przypadek, którego mi brakuje ... Nie wydaje mi się, że mogę użyć hipotez.

Pomoc będzie mile widziana.

— codd
źródło

@Gilles bardzo dobrze zrobione z edycją. Nie wiedziałem, że silnik TeX SE był w stanie to wszystko ... :-)

— codd

Czy się mylę, czy ćwiczenie zostało zaczerpnięte z „Typów i języków programowania” Pierce'a?

— Fabio F.,

@FabioF. Rzeczywiście pochodzi z książki Pierce's Types and Programming Languages. Dostarcza dowód, który wydaje mi się niejasny, ze względu na sposób, w jaki wykonuje indukcję. Dlatego sam próbowałem to udowodnić poprzez indukcję konstrukcji. Zastanawiałem się, czy nie wspomnieć, że pochodzi z książki, ale pomyślałem, że byłoby to raczej nieistotne. Jednak dobrze zauważony!

— codd

Odpowiedzi:

Okej, więc rozważmy przypadek, że , wyprowadzono stosując regułę E-If a jest uzyskany przez zastosowanie zasady E-Funny SO gdzie i gdzie . $r = \mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ $s$ $t$ $s = \mathtt{if}\: t'_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ $t_1 \rightarrow t'_1$ $t = \mathtt{if}\: t_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$ $t_2 \rightarrow t'_2$

nas szukasz . wynika z reguły E-Funny i wynika z reguły E-If. $u$ $u = \mathtt{if}\: t'_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$ $s \rightarrow u$ $t \rightarrow u$

— sepp2k
źródło

Pokonaj mnie do tego. Dobra robota.

— Patrick87

Boże, naprawdę szukałem za daleko ... Dzięki!

— codd

Ci mieszać je jednak,

wynika z e-Zabawne. Czy widzę coś nie tak?

s \to u

$s \rightarrow u$

— codd

@Jeroen Masz rację - wymieszałem je. Naprawiono teraz.

— sepp2k

Trochę terminologii może pomóc, jeśli chcesz to sprawdzić: te reguły przepisują reguły , nie mają one nic wspólnego z systemami typów¹. Właściwość, którą próbujesz udowodnić, nazywa się zbieżnością ; a dokładniej, jest to silne zbieżność : jeśli termin można skrócić na różne sposoby na jednym etapie, mogą one zbiegać się na następnym etapie. W ogólności, nie pozwala na zbiegu być dowolną liczbę etapów, a nie tylko: jeżeli i następnie jest tak, że i $r\to^*s$ $r\to^*t$ $u$ $s\to^*u$ $t\to^*u$ - jeśli termin może zostać skrócony na różne sposoby, bez względu na to, jak daleko się rozeszli, mogą w końcu z powrotem się zjednoczyć.

Najlepszym sposobem na udowodnienie właściwości takich indukcyjnie określonych reguł przepisywania jest indukcja nad strukturą wyprowadzenia redukcji, a nie przez strukturę skróconego terminu. Tutaj albo działa, ponieważ reguły są zgodne ze strukturą terminu lewostronnego, ale rozumowanie reguł jest prostsze. Zamiast zagłębiać się w ten termin, bierzesz wszystkie pary zasad i widzisz, który termin może być lewą stroną dla obu. W tym przykładzie otrzymasz te same przypadki na końcu, ale nieco szybciej.

W przypadku, który powoduje problemy, jedna strona zmniejsza część „if”, a druga strona zmniejsza część „wtedy”. Nie ma nakładania się między dwiema zmieniającymi się częściami ( w [E-If], w [E-IfFunny]), i nie ma ograniczenia na w [E-If] lub w [E- IfFunny]. Więc jeśli masz termin, do którego odnoszą się obie zasady - który musi mieć formę $t1$ $t_2$ $t_2$ $t_1$ , możesz zastosować reguły w dowolnej kolejności: $\mathtt{if}\: r_1 \:\mathtt{then}\: r_2 \:\mathtt{else}\: r_3$

\begin{array}{rcl} i f r_{1} t h e n r_{2} e l s e r_{3} \\ [E-If] ↙ & ↘ [E-IfFunny] \\ i f r_{1}^{'} t h e n r_{2} e l s e r_{3} & i f r_{1} t h e n r_{2}^{'} e l s e r_{3} \\ [E-IfFunny] ↘ & ↙ [E-If] \\ i f r_{1}^{'} t h e n r_{2}^{'} e l s e r_{3} \end{array}

$\begin{array}{rcl} & \mathtt{if}\: r_1 \:\mathtt{then}\: r_2 \:\mathtt{else}\: r_3 & \\ {\small \text{[E-If]}} \swarrow & & \searrow {\small \text{[E-IfFunny]}} \\ \mathtt{if}\: r_1' \:\mathtt{then}\: r_2 \:\mathtt{else}\: r_3 & & \mathtt{if}\: r_1 \:\mathtt{then}\: r_2' \:\mathtt{else}\: r_3 \\ {\small \text{[E-IfFunny]}} \searrow & & \swarrow {\small \text{[E-If]}} \\ & \mathtt{if}\: r_1' \:\mathtt{then}\: r_2' \:\mathtt{else}\: r_3 & \\ \end{array}$

¹ _{Czasami zobaczysz typy i przepisywanie razem, ale w ich istocie są to koncepcje ortogonalne.}

— Gilles „SO- przestań być zły”
źródło