Jaki jest sens konwersji

Myślę, że tego nie rozumiem, ale konwersja wygląda na mnie jako konwersja β , która nic nie robi, szczególny przypadek konwersji β, w której wynikiem jest tylko termin z abstrakcji lambda, ponieważ nie ma nic do zrobienia, rodzaj bezcelowej konwersji β .$\eta$$\beta$$\beta$$\beta$

Może więc konwersja jest czymś naprawdę głębokim i odmiennym od tego, ale jeśli tak, to nie rozumiem i mam nadzieję, że możesz mi w tym pomóc.$\eta$

(Dziękuję i przepraszam, wiem, że to część podstawowych zasad rachunku lambda)

Aktualizacja [2011-09-20]: Rozszerzyłem akapit o rozszerzeniu i ekstensywności. Dziękujemy Antonowi Salikhmetovowi za wskazanie dobrych referencji.$\eta$

-konwersja ( λ x . f x ) = f jest szczególnym przypadkiem β - konwersjitylkow szczególnym przypadku, gdy f jest samo w sobie abstrakcją, np. jeśli f = λ y . y y następnie ( λ x . f x ) = ( λ x . ( λ y . y y ) x ) = β ( λ x $\eta$$(\lambda x . f x) = f$$\beta$$f$$f = \lambda y . y y$Ale co jeśli f jest zmienną lub aplikacją, która nie sprowadza się do abstrakcji?

$$(\lambda x . f x) = (\lambda x . (\lambda y . y y) x) =_\beta (\lambda x . x x) =_\alpha f.$$ $f$

W pewnym sensie zasada jest jak szczególny rodzaj ekstensywności, ale musimy być nieco ostrożni, jak to jest stwierdzone. Możemy określić ekstensywność jako:$\eta$

1. dla wszystkich terminali M i N , jeśli M x = N x, to M = N lub$\lambda$$M$$N$$M x = N x$$M = N$
2. dla wszystkich jeśli ∀ x . f x = g x, a następnie f = g .$f, g$$\forall x . f x = g x$$f = g$

Pierwszy to meta-stwierdzenie dotyczące warunków rachunku. W nim x pojawia się jako zmienna formalna, tzn. Jest częścią rachunku λ . Można to udowodnić na podstawie reguł β η , patrz na przykład Twierdzenie 2.1.29 w „Rachunku lambda: jego składnia i semantyka” Barendregta (1985). Można to rozumieć jako stwierdzenie o wszystkich definiowalnych funkcjach, tj. Tych, które są oznaczeniami terminów λ .$\lambda$$x$$\lambda$$\beta\eta$$\lambda$

Drugim stwierdzeniem jest to, w jaki sposób matematycy zazwyczaj rozumieją wyrażenia matematyczne. Teoria -kalkusa opisuje pewien rodzaj struktur, nazwijmy je „ modelami λ ”. Model λ może być niepoliczalny, więc nie ma gwarancji, że każdy jego element odpowiada termowi λ (tak jak jest więcej liczb rzeczywistych niż wyrażeń opisujących liczby rzeczywiste). Ekstensywność mówi wtedy: jeśli weźmiemy dwie rzeczy f i g w modelu λ , jeśli f x = g x dla wszystkich x w modelu, to f = $\lambda$$\lambda$$\lambda$$\lambda$$f$$g$$\lambda$$f x = g x$$x$$f = g$. Teraz nawet jeśli model spełnia regułę , nie musi spełniać ekstensywności w tym sensie. (Potrzebne jest tutaj odniesienie i myślę, że musimy uważać na interpretację równości.)$\eta$

Istnieje kilka sposobów motywowania konwersji i η . Ja losowo wybrać jedną kategorię-teoretyczny, ukrytego jako λ -calculus, a ktoś inny nie może tłumaczyć z innych powodów.$\beta$$\eta$$\lambda$

Rozważmy wpisany calculus (ponieważ jest mniej mylący, ale mniej więcej takie samo rozumowanie działa dla niepypisanego λ- calculus). Jednym z podstawowych praw, które powinny posiadanych jest prawo wykładniczy C × B ≅ ( C B ) . (Używam notacji A → B i B A zamiennie, wybierając coś, co wydaje się wyglądać lepiej.) Co oznaczają izomorfizmy i : C A × B → ( C B ) A i 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$ wygląda jak napisane w λ- rachunku? Prawdopodobnie byłyby i = X F : C x B . λ : . λ b : B . f ⟨ , b ⟩ i J = λ g : ( C, B ) . λ 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$$ Krótki obliczenie z parą p -reductions (włączając w to P -reductions gatunku 1 ⟨ a , b ⟩ = a i gatunku 2 ⟨ a , b ⟩ = b produktów) mówi, że dla każdego g : ( C, B ) A mamy 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$ Od I i J są odwrotne od siebie oczekujemy i ( j g ) = g , ale faktycznie to udowodnić musimy użyć η -redukcja dwukrotnie: I ( j g ) = ( λ w : . X B : B . g a b ) = η $$i (j g) = \lambda a : A . \lambda b : B . g a b.$$ $i$$j$$i (j g) = g$$\eta$ Jest to jeden z powodówobniżenia η . Ćwiczenie: którareguła η jest potrzebna, aby pokazać, że 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$

Aby odpowiedzieć na to pytanie, możemy podać następujący cytat z odpowiedniej monografii „Rachunek lambda. Jego składnia i semantyka ”(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$

[Jego dowód opiera się na następującym twierdzeniu.]

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

$\lambda\eta$

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

Teorie HP-complete [za Hilbertem-Post] odpowiadają maksymalnym spójnym teoriom w teorii modeli dla logiki pierwszego rzędu.

Wystarczy dodać do bardzo dobrej odpowiedzi Andreja: teorii nietypowego $\lambda$Rachunek z $\beta$ i $\eta$ zasady redukcji spełniają niektóre bardzo ładne właściwości:

• Jest spójny w tym sensie, że istnieją na przykład dwa terminy$\lambda x y.x$ i $\lambda x y.y$które nie są $\beta\eta$odpowiednik. Jest to konsekwencja twierdzenia o zbiegu dla$\beta\eta$ zmniejszenie.

• Jest to maksymalna spójna teoria w następującym znaczeniu: if$\iota$jest
  relacją równoważności na takich warunkach, że:

  1. Jest zamknięty przez zgodność: $u\ =_\iota\ v \Rightarrow t\ u\ =_\iota\ t\ v$ itp.

  2. Jest równy 2 non$\beta\eta$równoważne terminy, które są normalnymi formami : istnieją$t$ i $u$ w normalnej formie, takiej jak $t=_\iota u$ i $t\neq_{\beta\eta}u$.

Zatem teoria jest niespójna : dla każdego terminu$t$, $u$ w normalnej formie $t=_{\beta\eta\iota}u$.

Jest to konsekwencja twierdzenia Böhm.

$\eta$-Redukcja ujmuje pojęcie ekstensywności - dwie funkcje są uważane za równe, jeśli dają te same wyniki na tych samych wejściach.

Jednym ze sposobów sformalizowania tego pojęcia jest: jeśli weźmiemy pod uwagę relację $=_{\beta \eta}$, przechodnie-refleksyjne zamknięcie relacji $\rightarrow_{\beta\eta}$, naturalne jest scharakteryzowanie tej relacji w kategoriach reguł wnioskowania teorii równań (np .: reguły formy: jeśli $M=N$, następnie $\lambda x.M = \lambda x.N$ i tak dalej - charakteryzowanie $=_{\beta}$ wymaga około 7 tego rodzaju zasad).

Teraz zastępuję $=_{\beta}$ z $=_{\beta\eta}$ sprowadza się do wprowadzenia aksjomatu $\lambda x. Mx = M$, which is equivalent to the extensionality rule: if $Mx=Nx$, then $M=N$. This is exactly the notion that two functions equal on all input arguments should be considered identical.