Równoważność jest po prostu równoważnością omawianej teorii równań . W tym przypadku jest to teoria przedstawiona w tabeli 1. Zauważ, że teoria ta nie obejmuje : uczyni to teorię ekstensywną, a ostatecznie chodzi o to, że szanuje intensywność , podczas gdy spowoduje CL częściowo ekstensywny. Nie jestem pewien, dlaczego druga odpowiedź wspomina .η ξ λ ηληξλη
Zauważ, że w :λ
(M=βN)⟹(λx.M=βλx.N)(1)
Powinno to być intuicyjnie oczywiste: jeśli jest -wymienialne na gdy stoi samo, to jest też -wymienialne na gdy jest podtermem .β N β N λ x . M.MβNβNλ x . M.
Regułę zdefiniowany jako
umożliwia bezpośrednie wnioskowanie, gdy jest częścią teorii . Jego analogiem CL będzie:
M.ξ λ M
M.( λ x . M)= N= ( λ x . N)( ξλ)
λM.( λ∗x . M.)= N= ( λ∗x . N.)( ξdoL.)
Chodzi o to, że w CL nie ma zastosowania :
( M=wN.) ⟹ ( λ∗x . M.=wλ∗x . N.)(2)
Innymi słowy, jeśli dwa terminy są słabo równe, to niekoniecznie jest tak w przypadku ich pseudoabstrakcyjnych wersji.
W związku z tym, jeśli dodamy do teorii CL, wówczas zaczniemy równanie terminów, które mają różne formy normalne.ξdoL.
Uwaga. Tutaj oznacza słabą równość. Oznacza to, że można przekonwertować na (i odwrotnie) poprzez serię i (prawdopodobnie również , jeśli jest to część teorii). Jak zapewne wiesz, jest analogiem CL dla .M N S K I = w = βM.=wN.M.N.S.K.ja=w=β
λ∗ to pseudoabstrakcja zdefiniowana na stronie 5 dokumentu. Ma następującą właściwość:
( λ∗x . M.) N⊳w[ N/ x]M(3)
Ta właściwość ułatwia znalezienie analogu CL dla dowolnego -termu: wystarczy zmienić na i zastosować tłumaczenia zgodnie z definicją .λ λ ∗ λ ∗λλλ∗λ∗
Dla jasności, „kontrprzykład” w tej odpowiedzi nie jest kontrprzykładem na (2). Ponieważ jeśli mamy:
N = ( λ ∗ z . Z ) x
M.= x(4)
N.= ( λ∗z. z) x(5)
Wtedy naprawdę oznacza (stosując tłumaczenia strony 5 oraz fakt, że jest zdefiniowany jako na końcu strony 4):I S K KN.jaS K K
N.= ( λ∗z. z) x = I x = S K K x(6)
Ponieważ , to w rzeczywistości ma to . Jeśli jednak jest to przeciwny przykład, powinniśmy mieć to . Ale jeśli tłumaczymy, w rzeczywistości otrzymujemy:M = w N ( λ ∗ y . M ) ≠ w ( λ ∗ y . N )S K K x ⊳wK x( K x) ⊳wxM.=wN.( λ∗y. M.) ≠w( λ∗y. N.)
( λ ∗ y . N ) = ( λ ∗ y . S K K x ) = K ( S K K x )
( λ∗y. M.) = ( λ∗y. x ) = K x(7)
( λ∗y. N.) = ( λ∗y. S K K x ) = K ( S K K x )(8)
Łatwo jest zweryfikować, że (7) i (8) są wciąż słabo równe, ponieważ:
K ( S K K x) ⊳wK ( K x( K x)) ⊳wK x(9)
Teraz właściwym przeciw-przykładem dla (2) byłoby:
N = x
M.= K x y
N.= x
Ponieważ , zdecydowanie ma to . Jeśli jednak przetłumaczysz ostrożnie wersje abstrakcji, zobaczysz, że obie są odrębnymi formami normalnymi - i nie mogą być przekształcalne zgodnie z twierdzeniem Church-Rosser.M = w NK xy⊳wxM.=wN.
Najpierw sprawdzamy :M.′
M′(λ∗x.Kxy)P⊳wPλ∗
M.′= λ∗x . K x y= S ( λ∗x . K x ) ( λ∗x . y)= S ( λ∗x.Kx)(Ky)=S(S(λ∗x.K)(λ∗x.x))(Ky)=S(S(λ∗x.K)(I))(Ky)=S(S(λ∗x.K)(SKK))(Ky)=S(S(KK)(SKK))(Ky)
Tutaj możesz sprawdzić, czy jest normalną formą.
Tutaj możesz sprawdzić, czy , jak można się spodziewać, jeśli ma zachowywać się jak abstrakcja dla CL.
M.′( λ∗x . K.x y) P⊳wP.λ∗
Teraz sprawdzamy :
N ′N.′
N.′= λ∗x . x= Ja= S K K
Która jest oczywiście normalną formą inną niż , więc według twierdzenia Church-Rosser. Należy również zauważyć, że , to znaczy i «wytwarzają taką samą moc» dla dowolnych wejść .M ′ ≠ w N ′ N ′ P ⊳ w P M ′ N ′ PM.′M.′≠wN.′N.′P.⊳wP.M.′N.′P.
Udowodniliśmy teraz, że (2) nie zachowuje się w CL i że teoria CL zawierająca zrównuje zatem warunki, które nie są słabo równe. Ale dlaczego nas to obchodzi?ξ
Przede wszystkim sprawia, że kombinacyjna interpretacja niedoskonała: najwyraźniej nie wszystkie właściwości metateoretyczne zostają przeniesione.λ
Ponadto, a może co ważniejsze, chociaż istnieją ekstensywne teorie i CL, są one pierwotnie i powszechnie utrzymywane w intensywności. Intiętność jest przyjemną właściwością, ponieważ obliczenia modelu i CL jako procesu, i z tej perspektywy dwa różne programy (konkretnie terminy o innej normalnej formie), które zawsze dają takie same wyniki (przy równych danych wejściowych), nie mogą być zrównane. szanuje tę zasadę w , a jeśli chcemy, aby rozszerzana, moglibyśmy po prostu dodać np. . Ale wprowadzenieλ ξ λ λ η ξ ξλλξλληξw CL nie czyni już tego całkowicie intensywnym (w rzeczywistości tylko częściowo). I to jest powód, dla „s«rozgłos», jak ujmuje to artykuł.ξ
EDYCJA Ta odpowiedź jest niepoprawna, jak słusznie zauważył drugi odpowiadający. Użyłem tłumaczenia na logikę kombinacyjną z Asperti i Longo, która subtelnie różni się od tej w Selinger.
W rzeczywistości ilustruje to kluczowy punkt: „kombinacyjna interpretacja” rachunku lambda nie jest jedną rzeczą! Różni autorzy robią to nieco inaczej.
Zostawiam tutaj swoją odpowiedź dla potomnych, ale druga odpowiedź jest lepsza.
Równoważność w tym kontekście jest zdefiniowana w tabelach 1 i 2 w pracy Selingera. Jednak nieco inna aksjatyzacja może nieco wyjaśnić.
To tak naprawdę oznacza, że dwa pojęcia są konwertowalne w teorii . Możemy zdefiniować „wymienialność” za pomocą następujących dwóch aksjomatów:λ
Plus, oczywiście, zwykłe aksjomaty i reguły wnioskowania potrzebne do przeprowadzenia kongruencją. Z tego powinno być oczywiste, że każdy kontrprzykład będzie polegał na warunku swobodnej zmiennej przy reguły .η= η
Myślę, że jest to prawdopodobnie najprostsze:
N = ( λ z . Z ) x
Możesz sam sprawdzić, czy , ale ich odpowiednie interpretacje kombinatoryczne nie są równe zgodnie z regułami w Tabeli 2.λ y. M.= λ y. N.
źródło