Zbieg ekspansji beta

Niech $\to_\beta$ będzie redukcją $\beta$ w rachunku $\lambda$ . Zdefiniuj $\beta$ rozszerzenie $\leftarrow_\beta$ przez $t'\leftarrow_\beta t \iff t\to_\beta t'$ .

Czy $\leftarrow_\beta$ zbieżny? Innymi słowy, nie mamy, że dla każdego $l,d,r$ , jeżeli $l \to_\beta^* d\leftarrow_\beta^* r$ , to istnieje $u$ taki sposób, że $l\leftarrow_\beta^* u \to_\beta^* r$ ?

Słowa kluczowe: zbieżność w górę, własność CR do góry nogami

Zacząłem od spojrzenia na słabszą właściwość: lokalną konfluencję (tj. Jeśli $l \to_\beta d\leftarrow_\beta r$ , to $l\leftarrow_\beta^* u \to_\beta^* r$ ). Nawet gdyby to była prawda, nie oznaczałoby to konfluencji, ponieważ rozszerzenie $\beta$ nie kończy się, ale pomyślałem, że pomoże mi to zrozumieć przeszkody.

(Góra) W przypadku, w którym obie redukcje są na górnym poziomie, hipoteza staje $(\lambda x_1.b_1)a_1\rightarrow b_1[a_1/x_1]=b_2[a_2/x_2]\leftarrow (\lambda x_2.b_2)a_2$ . Aż do nazw $\alpha$ , możemy założyć, że $x_1\not =x_2$ i że pod tym względem ani $x_1$ ani $x_2$ jest darmowe.

(Rzut) Jeśli $x_1$ nie jest wolny w $b_1$ mamy $b_1=b_2[a_2/x_2]$ , a zatem $(\lambda x_1.b_1)a_1=(\lambda x_1.b_2[a_2/x_2])a_1\leftarrow(\lambda x_1.(\lambda x_2.b_2)a_2)a_1\rightarrow (\lambda x_2.b_2)a_2$ .

Naiwny dowód indukcyjny (na $b_1$ i $b_2$ ) dla sprawy (u góry) byłby następujący:

Jeśli $b_1$ jest zmienną $y_1$ ,
- Jeśli $y_1=x_1$ hipoteza staje $(\lambda x_1.x_1)a_1\rightarrow a_1=b_2[a_2/x_2]\leftarrow (\lambda x_2.b_2)a_2$ , i faktycznie mają $(\lambda x_1.x_1)a_1=(\lambda x_1.x_1)(b_2[a_2/x_2])\leftarrow (\lambda x_1.x_1)((\lambda x_2.b_2)a_2)\rightarrow (\lambda x_2.b_2)a_2$ .
- Jeśli $y_1\not=x_1$ , możemy po prostu użyć (Rzut).
Obowiązują te same dowody, ponieważ $b_2$ jest zmienną.
Dla $b_1=\lambda y.c_1$ i $b_2=\lambda y.c_2$ hipoteza staje $(\lambda x_1.\lambda y. c_1)a_1\rightarrow \lambda y.c_1[a_1/x_1]=\lambda y.c_2[a_2/x_2]\leftarrow (\lambda x_2.\lambda y.c_2)a_2$ i hipoteza indukcyjna daje $d$ takie, że $(\lambda x_1.c_1)a_1\leftarrow d\rightarrow (\lambda x_2.c_2)a_2$ co oznacza, że $\lambda y.(\lambda x_1.c_1)a_1\leftarrow \lambda y.d\rightarrow \lambda y.(\lambda x_2.c_2)a_2$ . Niestety nie mamy $\lambda y.(\lambda x_2.c_2)a_2\rightarrow (\lambda x_2.\lambda y.c_2)a_2$ . (To sprawia, że myślę oredukcji $\sigma$ .)
Podobny problem pojawia się w przypadku aplikacji: $\lambda$ nie są tam, gdzie powinny być.

lambda-calculus term-rewriting

— xavierm02
źródło

@chi O ile się nie mylę,

działa.

(λ b . y b) y \leftarrow (λ a . (λ b . a b) y) y \to (λ a . a y) y

$(\lambda b.yb)y\leftarrow(\lambda a. (\lambda b. a b)y)y\rightarrow (\lambda a. a y)y$

— xavierm02

W pewnym stopniu zgadzam się z @chi, że wydaje się zbieżny po tym, jak o tym pomyślisz i zobaczysz kilka kontrprzykładów. Ale właściwie co z

(λ x . x x y) y \to y y y \leftarrow (λ x . y x x) y

$(\lambda x.x\;x\;y)\;y \to y\;y\;y \leftarrow (\lambda x.y\;x\;x)\;y$

— Rodolphe Lepigre

Chociaż byłoby to dla mnie wygodne, gdyby to była prawda, jestem trochę bardziej pesymistą. Mój kolega poczynił następującą uwagę, która sprawia, że wydaje się to mało prawdopodobne: oznaczałoby to, że można połączyć dowolne dwa dowolne programy obliczające tę samą liczbę całkowitą (kościelną).

— xavierm02

Odpowiedź brzmi nie. Ćwiczenie 3.5.11 w Barendregt daje przeciwny przykład przypisany Plotkinowi, ale bez odniesienia:

oraz

. Poszukam dowodu.

(λ x . b x (b c)) c

$(\lambda x. b x (b c)) c$

(λ x . x x) (b c)

$(\lambda x. x x) (b c)$

— Gilles 'SO - przestań być zły'

Zamieściłem kontrprzykład jako odpowiedź z tym, co uważałem za dowód, ale jest krok, którego nie potrafię zrozumieć. Jeśli ktoś może to rozgryźć, proszę opublikować odpowiedź, a ja ją usunę.

— Gilles „SO- przestań być zły”

Odpowiedzi:

Dwa kontrprzykłady to:

$(\lambda x. b x (b c)) c$ oraz $(\lambda x. x x) (b c)$ (Plotkin).
$(\lambda x. a (b x)) (c d)$ i $a ((\lambda y. b (c y)) d)$ (Van Oostrom).

Kontrprzykład opisany poniżej podano w The Lambda Calculus: Its Syntax and Semantics autorstwa HP Barenredgt, wydanie poprawione (1984), ćwiczenie 3.5.11 (vii). Jest to przypisywane Plotkinowi (bez dokładnego odniesienia). Daję niekompletny dowód, który został zaadaptowany z dowodu Vincenta van Oostroma z innego kontrprzykładu, w Take Five: an Easy Expansion Exercise (1996) [PDF] .

Podstawą dowodu jest twierdzenie o standaryzacji, które pozwala nam rozważać tylko rozszerzenia beta pewnej formy. Intuicyjnie mówiąc, standardowa redukcja to redukcja, która powoduje wszystkie jej skurcze od lewej do prawej. Dokładniej, taka redukcja jest niestandardowy IFF jest krok $M_i$ którego REDEX jest rezydualną Redex do lewej strony Redex poprzedniego kroku $M_j$ ; „Lewy” i „prawy” dla redeksu są zdefiniowane przez pozycję $\lambda$ która jest eliminowana, gdy redeks jest kurczony. Twierdzenie o standaryzacji stwierdza, że jeśli $M \rightarrow_\beta^* N$ to występuje standardowa redukcja z $M$ do $N$ .

Niech $L = (\lambda x. b x (b c)) c$ oraz $R = (\lambda x. x x) (b c)$ . Oba terminy beta zmniejszają się do $b c (b c)$ w jednym kroku.

Załóżmy, że istnieje wspólny przodek takie, że . Dzięki twierdzeniu o standaryzacji możemy założyć, że obie redukcje są standardowe. Bez utraty ogólności, załóżmy, że jest pierwszym krokiem, w którym różnice te są różne. Z tych dwóch redukcji, niech będzie tą, w której redeks pierwszego kroku znajduje się na lewo od drugiego, i napisz gdzie $A$ $L \leftarrow_\beta^* A \rightarrow_\beta^* R$ $A$ $\sigma$ $A = C_1[(\lambda z. M) N]$ $C_1$ jest kontekstem tego skurczu, a $(\lambda z. M) N$ to redeks. Niech $\tau$ będzie drugą redukcją.

Ponieważ $\tau$ jest standardem, a jego pierwszym krokiem jest na prawo od dołka w $C_1$ , nie może się skurczyć na $C_1$ ani na lewo od niego. W związku z tym ostateczny termin $\tau$ ma postać $C_2[(\lambda z. M') N']$ , gdzie część $C_1$ i $C_2$ na lewo od ich otworów są identyczne, $M \rightarrow_\beta^* M'$ i $N \rightarrow_\beta^* N'$ . Ponieważ $\sigma$ zaczyna się od zmniejszenia przy $C_1$ i nigdy nie zmniejsza się dalej w lewo, jego końcowy człon musi mieć postać $C_3[S]$ gdzie część $C_3$ na lewo od jego otworu jest identyczna z lewą częścią $C_1$ i $C_2$ , a $M[z \leftarrow N] \rightarrow_\beta^* S$ .

Zauważ, że każdy z $L$ i $R$ zawiera pojedynczą lambdę, która znajduje się po lewej stronie operatora aplikacji na najwyższym poziomie. Ponieważ $\tau$ zachowuje lambda $\lambda z. M$ , to Lambda jest w zależności od tego, jeden z $L$ lub $R$ jest ostatni termin $\tau$ i w tym okresie argument zastosowania otrzymuje się przez redukcję $N$ . Redeks znajduje się na najwyższym poziomie, co oznacza, że $C_1 = C_2 = C_3 = []$ .

Jeśli $\tau$ kończy się na $R$ , to $M \rightarrow_\beta^* z z$ , $N \rightarrow_\beta^* b c$ i $M[z \leftarrow N] \rightarrow_\beta^* (\lambda x. b x (b c)) c$ . Jeżeli $N$ ma zstępnych $L$ wówczas potomek musi zmniejszyć do $b c$ , która jest normalnie postać $N$ . W szczególności brak potomka $N$ może być lambda tak $\sigma$ nie może zawrzeć subterm formy , gdzie jest potomkiem . Ponieważ jedynym subterm z , który redukuje się do jest , jedyną możliwą potomkiem w jest jedynym występowanie siebie. $\check{N} P$ $\check{N}$ $N$ $L$ $b c$ $b c$ $N$ $L$ $b c$
Jeśli $\tau$ kończy się na $L$ , to $M \rightarrow_\beta^* b z (b c)$ , $N \rightarrow_\beta^* c$ i $M[z \leftarrow N] \rightarrow_\beta^* (\lambda x. x x) (b c)$ . Jeśli $N$ ma potomka w $R$ potomek ten musi również zredukować do $c$ przez zbieg.

W tym momencie, wniosek powinien być zgodny z łatwością według van Oostrom, ale jestem czegoś brakuje: Nie widzę jak śledzenie potomków $N$ daje żadnych informacji o $M$ . Przepraszamy za niekompletny post, pomyślę o tym z dnia na dzień.

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

$\beta$ $x$ $v$ $(\lambda x.v)\;t_1 \to_\beta v$ $(\lambda x.v)\;t_2 \to_\beta v$ $t_1$ $t_2$ $\beta$ $t_1$ $t_2$ $u$ $u \to_\beta^\ast t_1$ $u \to_\beta^\ast t_2$

— Rodolphe Lepigre
źródło

(λ x . v) t_{1} \leftarrow (λ x . (λ x . v) t_{1}) t_{2} \to (λ x . v) t_{2}

$(\lambda x .v) t_1\leftarrow (\lambda x .(\lambda x .v) t_1)t_2\rightarrow (\lambda x .v) t_2$

Cholera, masz rację! Później spróbuję wymyślić coś innego, nie mam teraz czasu.

— Rodolphe Lepigre