Logika kombinacyjna - Combinatory logic

Logika kombinatoryczna to zapis eliminujący potrzebę zmiennych ilościowych w logice matematycznej . Został wprowadzony przez Mosesa Schönfinkela i Haskella Curry'ego , a ostatnio był używany w informatyce jako teoretyczny model obliczeń, a także jako podstawa do projektowania funkcjonalnych języków programowania . Opiera się na kombinatorach, które Schönfinkel wprowadził w 1920 r. z myślą o zapewnieniu analogicznego sposobu budowania funkcji – i usunięcia jakiejkolwiek wzmianki o zmiennych – zwłaszcza w logice predykatów . Kombinator to funkcja wyższego rzędu, która używa tylko aplikacji funkcji i wcześniej zdefiniowanych kombinatorów do zdefiniowania wyniku na podstawie swoich argumentów.

W matematyce

Logika kombinacyjna była pierwotnie pomyślana jako „przed-logika”, która wyjaśniałaby rolę zmiennych ilościowych w logice, zasadniczo poprzez ich eliminację. Innym sposobem eliminacji zmiennych kwantyfikowanych jest funktor logiki predykatów Quine'a . Podczas gdy moc wyrazu logiki kombinatorycznej zazwyczaj przewyższa moc logiki pierwszego rzędu , moc wyrazu logiki funktora predykatów jest identyczna jak logiki pierwszego rzędu ( Quine 1960, 1966, 1976 ).

Pierwotny wynalazca logiki kombinatorycznej, Moses Schönfinkel , nie opublikował nic na temat logiki kombinatorycznej po swoim pierwszym artykule z 1924 roku. Haskell Curry odkrył na nowo kombinatory pracując jako wykładowca na Uniwersytecie Princeton pod koniec 1927 roku. Pod koniec lat 30. Alonzo Church i jego studenci z Princeton wynaleźli konkurencyjny formalizm dla abstrakcji funkcjonalnej, rachunek lambda , który okazał się bardziej popularny niż logika kombinacyjna. Skutek tych historycznych uwarunkowań był taki, że dopóki teoretyczna informatyka nie zaczęła interesować się logiką kombinatoryczną w latach 60. i 70., prawie wszystkie prace na ten temat wykonali Haskell Curry i jego uczniowie lub Robert Feys w Belgii . Curry i Feys (1958) oraz Curry i in. (1972) badają wczesną historię logiki kombinatorycznej. Aby uzyskać bardziej nowoczesne podejście do logiki kombinatorycznej i rachunku lambda, zobacz książkę Barendregta , w której przegląda modele opracowane przez Danę Scott dla logiki kombinatorycznej w latach 60. i 70. XX wieku.

W informatyce

W informatyce logika kombinatoryczna jest wykorzystywana jako uproszczony model obliczeń , stosowany w teorii obliczalności i teorii dowodu . Pomimo swojej prostoty, logika kombinatoryczna wychwytuje wiele istotnych cech obliczeń.

Logika kombinatoryczna może być postrzegana jako wariant rachunku lambda , w którym wyrażenia lambda (reprezentujące abstrakcję funkcjonalną) zastępuje się ograniczonym zbiorem kombinatorów , funkcji pierwotnych bez wolnych zmiennych . Przekształcenie wyrażeń lambda w wyrażenia kombinatora jest łatwe, a redukcja kombinatora jest znacznie prostsza niż redukcja lambda. Stąd logika kombinacyjna została wykorzystana do modelowania niektórych nieścisłych języków programowania funkcjonalnego i sprzętu . Najczystszą formą tego poglądu jest język programowania Unlambda , którego jedynymi prymitywami są kombinatory S i K rozszerzone o wejście/wyjście znakowe. Chociaż nie jest to praktyczny język programowania, Unlambda ma pewne teoretyczne zainteresowanie.

Logika kombinacyjna może mieć różne interpretacje. Wiele wczesnych prac Curry'ego pokazało, jak przełożyć zbiory aksjomatów dla logiki konwencjonalnej na równania logiki kombinatorycznej (Hindley i Meredith 1990). Dana Scott w latach 60. i 70. pokazała, jak połączyć teorię modeli i logikę kombinatoryczną.

Podsumowanie rachunku lambda

Rachunek lambda dotyczy obiektów zwanych wyrażeniami lambda , które mogą być reprezentowane przez następujące trzy formy łańcuchów:

• ${\displaystyle v}$
• ${\ Displaystyle \ lambda v.E_ {1}}$
• ${\displaystyle (E_{1}E_{2})}$

gdzie jest nazwą zmiennej wyprowadzoną z predefiniowanego nieskończonego zbioru nazw zmiennych i są wyrażeniami lambda. ${\displaystyle v}$${\displaystyle E_{1}}$${\displaystyle E_{2}}$

Terminy formularza nazywane są abstrakcjami . Zmienna v nazywana jest formalnym parametrem abstrakcji i jest ciałem abstrakcji. Termin reprezentuje funkcję, która zastosowana do argumentu wiąże parametr formalny v z argumentem, a następnie oblicza wynikową wartość — to znaczy zwraca , przy czym każde wystąpienie v jest zastępowane przez argument. ${\ Displaystyle \ lambda v.E_ {1}}$${\displaystyle E_{1}}$${\ Displaystyle \ lambda v.E_ {1}}$${\displaystyle E_{1}}$${\displaystyle E_{1}}$

Warunki formularza nazywane są wnioskami . Aplikacje modelują wywołanie lub wykonanie funkcji: funkcja reprezentowana przez ma zostać wywołana, z jej argumentem, a wynik jest obliczany. Jeśli (czasami nazywany applicand ) jest abstrakcją, termin może być skrócony : argument może być podstawiony do ciała w miejsce formalnego parametru , a wynikiem jest nowy termin lambda, który jest odpowiednikiem starego jeden. Jeśli wyraz lambda nie zawiera podwarunków postaci, to nie można go zredukować i mówi się, że ma postać normalną . ${\displaystyle (E_{1}E_{2})}$${\displaystyle E_{1}}$${\displaystyle E_{2}}$${\displaystyle E_{1}}$${\displaystyle E_{2}}$${\displaystyle E_{1}}$${\displaystyle E_{1}}$${\ Displaystyle ((\ lambda v.E_ {1}) E_ {2})}$

Wyrażenie reprezentuje wynik wzięcia terminu E i zastąpienia w nim wszystkich wolnych wystąpień v przez a . Tak piszemy ${\displaystyle E[v:=a]}$

${\ Displaystyle ((\ Lambda VE) a) \ Strzałka w prawo E [v: = a]}$

Zgodnie z konwencją, przyjmujemy jako skrót (tj. aplikacja pozostaje asocjacyjna ). ${\ Displaystyle (abc)}$${\ Displaystyle ((ab) c)}$

Motywacją tej definicji redukcji jest to, że ujmuje ona podstawowe zachowanie wszystkich funkcji matematycznych. Rozważmy na przykład funkcję obliczającą kwadrat liczby. Możemy napisać

Kwadrat x to${\displaystyle x*x}$

(Użycie " " do wskazania mnożenia.) x tutaj jest formalnym parametrem funkcji. Aby obliczyć kwadrat dla konkretnego argumentu, powiedzmy 3, wstawiamy go do definicji w miejsce parametru formalnego: ${\ Displaystyle *}$

Kwadrat 3 to ${\displaystyle 3*3}$

Aby ocenić wynikowe wyrażenie , musielibyśmy odwołać się do naszej wiedzy o mnożeniu i liczbie 3. Ponieważ każde obliczenie jest po prostu złożeniem oceny odpowiednich funkcji na odpowiednich argumentach pierwotnych, ta prosta zasada podstawienia wystarcza do uchwycenia zasadniczego mechanizmu obliczenie. Co więcej, w rachunku lambda pojęcia takie jak „3” i „ ” mogą być reprezentowane bez potrzeby stosowania zewnętrznie zdefiniowanych operatorów pierwotnych lub stałych. W rachunku lambda można zidentyfikować terminy, które odpowiednio zinterpretowane zachowują się jak liczba 3 i jak operator mnożenia, qv Church Encoding . ${\displaystyle 3*3}$${\ Displaystyle *}$

Rachunek lambda jest znany z tego, że pod względem mocy obliczeniowej jest równoważny wielu innym wiarygodnym modelom obliczeniowym (w tym maszynom Turinga ); to znaczy, że wszelkie obliczenia, które można wykonać w dowolnym z tych innych modeli, można wyrazić w rachunku lambda i na odwrót. Zgodnie z tezą Churcha-Turinga oba modele mogą wyrażać dowolne możliwe obliczenia.

Być może zaskakujące jest to, że rachunek lambda może reprezentować dowolne wyobrażalne obliczenia przy użyciu tylko prostych pojęć abstrakcji funkcji i aplikacji opartych na prostym podstawieniu terminów za pomocą tekstu na zmienne. Ale jeszcze bardziej niezwykłe jest to, że abstrakcja nie jest nawet wymagana. Logika kombinatoryczna to model obliczeń równoważny rachunku lambda, ale bez abstrakcji. Zaletą tego jest to, że obliczanie wyrażeń w rachunku lambda jest dość skomplikowane, ponieważ semantyka podstawienia musi być określona z dużą ostrożnością, aby uniknąć problemów z przechwytywaniem zmiennych. W przeciwieństwie do tego, ocenianie wyrażeń w logice kombinatorycznej jest znacznie prostsze, ponieważ nie ma pojęcia podstawienia.

Rachunki kombinacyjne

Ponieważ abstrakcja jest jedynym sposobem wytwarzania funkcji w rachunku lambda, coś musi ją zastąpić w rachunku kombinatorycznym. Zamiast abstrakcji, rachunek kombinatoryczny dostarcza ograniczonego zestawu funkcji pierwotnych, z których można zbudować inne funkcje.

Terminy kombinacyjne

Termin kombinacyjny ma jedną z następujących form:

Składnia	Nazwa	Opis
x	Zmienny	Znak lub ciąg reprezentujący termin kombinacyjny.
P	Funkcja prymitywna	Jeden z symboli kombinatora I , K , S .
(MN)	Podanie	Stosowanie funkcji do argumentu. M i N są terminami kombinacyjnymi.

Funkcje pierwotne są kombinatorami lub funkcjami, które, gdy są postrzegane jako wyrażenia lambda, nie zawierają wolnych zmiennych .

Aby skrócić zapisy, ogólną konwencją jest to , że , a nawet , oznacza termin . Jest to ta sama ogólna konwencja (lewostronna asocjatywność), jak w przypadku wielokrotnych zastosowań w rachunku lambda. ${\displaystyle (E_{1}E_{2}E_{3}...E_{n})}$${\displaystyle E_{1}E_{2}E_{3}...E_{n}}$${\displaystyle (...((E_{1}E_{2})E_{3})...E_{n})}$

Redukcja logiki kombinatorycznej

W logice kombinatorycznej każdy kombinator pierwotny ma regułę redukcji postaci

( P x ₁ ... x _n ) = E

gdzie E jest terminem wymieniającym tylko zmienne ze zbioru { x ₁ ... x _n } . W ten sposób prymitywne kombinatory zachowują się jak funkcje.

Przykłady kombinatorów

Najprostszym przykładem kombinatora jest I , kombinator tożsamości, zdefiniowany przez

( I x ) = x

dla wszystkich terminów x . Innym prostym kombinatorem jest K , który tworzy funkcje stałe: ( K x ) jest funkcją, która dla dowolnego argumentu zwraca x , więc mówimy

(( K x ) y ) = x

dla wszystkich terminów x i y . Lub, zgodnie z konwencją wielokrotnego stosowania,

( K x y ) = x

Trzecim kombinatorem jest S , który jest uogólnioną wersją aplikacji:

( S x yz ) = ( xz ( yz ))

S stosuje x do y po pierwszym podstawieniu z do każdego z nich. Innymi słowy, x jest stosowane do y wewnątrz środowiska z .

Biorąc pod uwagę S i K , samo I jest niepotrzebne, ponieważ można je zbudować z pozostałych dwóch:

(( SKK ) x )

= ( SKK x )

= ( K x ( K x ))

= x

dla dowolnego terminu x . Należy zauważyć, że chociaż (( SKK ) x ) = ( I x ) w odniesieniu do X ( SKK ) sama nie jest równy I . Mówimy, że warunki są ekstensywnie równe . Równość rozszerzalna ujmuje matematyczne pojęcie równości funkcji: dwie funkcje są równe, jeśli zawsze dają te same wyniki dla tych samych argumentów. W przeciwieństwie do tego, same terminy, wraz z redukcją kombinatorów pierwotnych, ujmują pojęcie intensjonalnej równości funkcji: że dwie funkcje są równe tylko wtedy, gdy mają identyczne implementacje aż do rozwinięcia kombinatorów pierwotnych. Istnieje wiele sposobów na zaimplementowanie funkcji tożsamości; ( SKK ) i ja jesteśmy wśród tych sposobów. ( SKS ) to kolejny. Użyjemy słowa równoważny, aby wskazać równość ekstensjonalną, zastrzegając równe dla identycznych terminów kombinatorycznych.

Bardziej interesującym kombinatorem jest kombinator punktu stałego lub kombinator Y , który można wykorzystać do implementacji rekurencji .

Kompletność bazy SK

S i K mogą być złożone w taki sposób, aby tworzyły kombinatory, które są ekstensywnie równe dowolnemu członowi lambda, a zatem, zgodnie z tezą Churcha, dowolnej funkcji obliczalnej. Dowodem jest przedstawienie transformacji T [ ], która konwertuje dowolny wyraz lambda na równoważny kombinator.

T [ ] można zdefiniować w następujący sposób:

1. T [ x ] => x
2. T [( E ₁ E ₂)] => ( T [ E ₁] T [ E ₂])
3. T [ λx . E ] => ( K T [ E ]) (jeśli x nie występuje w E )
4. T [ λx . x ] => I
5. T [ λx . λy . E ] => T [ λx . T [ λ y . E ]] (jeśli x występuje w E )
6. T [ λx . ( E ₁ e ₂)] => ( S , T [ λx . E ₁] T [ λx . E₂ ]) (jeśli x występuje wolna w E ₁ lub E ₂)

Zauważ, że T [ ] nie jest dobrze wpisaną funkcją matematyczną, ale raczej przepisem terminów: Chociaż ostatecznie daje kombinator, transformacja może generować wyrażenia pośredniczące, które nie są ani terminami lambda, ani kombinatorami, poprzez regułę (5).

Proces ten jest również znany jako eliminacja abstrakcji . Ta definicja jest wyczerpująca: każde wyrażenie lambda będzie podlegać dokładnie jednej z tych reguł (patrz Podsumowanie rachunku lambda powyżej).

Jest to związane z procesem abstrahowania nawiasów , który przyjmuje wyrażenie E zbudowane ze zmiennych i aplikacji i tworzy wyrażenie kombinator [x]E, w którym zmienna x nie jest wolna, tak że zachodzi [ x ] E x = E. Bardzo prosty algorytm abstrakcji nawiasów jest definiowany przez indukcję na strukturze wyrażeń w następujący sposób:

1. [ x ] y  := K y
2. [ x ] x  := I
3. [ x ]( E₁ E₂ ) := S ([ x ] E₁ )([ x ] E₂ )

Abstrakcja nawiasów indukuje translację z terminów lambda do wyrażeń kombinatora, interpretując abstrakcje lambda przy użyciu algorytmu abstrakcji nawiasów.

Konwersja wyrazu lambda na równoważny wyraz kombinatoryczny

Na przykład skonwertujemy wyraz lambda λx . λy .( y x ) do wyrażenia kombinatorycznego:

T [ λx . λy .( y x )]

= T [ λx . T [ λy .( y x )]] (o 5)

= T [ λx .( S T [ λy . y ] T [ λy . x ])] (przez 6)

= T [ λx .( SI T [ λy . x ])] (przez 4)

= T [ λx .( SI ( K T [ x ]))] (przez 3)

= T [ λx .( SI ( K x ))] (przez 1)

= ( S T [ λx .( SI )] T [ λx .( K x )]) (przez 6)

= ( S ( K ( SI )) T [ λx .( K x )]) (przez 3)

= ( S ( K ( SI )) ( S T [ λx . K ] T [ λx . x ])) (przez 6)

= ( S ( K ( SI )) ( S ( KK ) T [ λ x . x ])) (przez 3)

= ( S ( K ( SI )) ( S ( KK ) I )) (przez 4)

Jeśli zastosujemy ten wyraz kombinatoryczny do dowolnych dwóch wyrazów x i y (poprzez wprowadzenie ich w sposób podobny do kolejki do kombinatora „od prawej”), zmniejszy się on w następujący sposób:

( S ( K ( S I )) ( S ( K K ) I ) xy)

= ( K ( S I ) x ( S ( K K ) I x) y)

= ( S I ( S ( K K ) I x) y)

= ( I y ( S ( K K ) I xy))

= (y ( S ( K K ) I xy))

= (y ( K K x ( I x) y))

= (y ( K ( I x) y))

= (y ( I x))

= (yx)

Reprezentacja kombinatoryczna ( S ( K ( SI ))( S ( KK ) I )) jest znacznie dłuższa niż reprezentacja jako wyraz lambda λx . λy .(yx). To jest typowe. Ogólnie rzecz biorąc, konstrukcja T [ ] może rozszerzać człon lambda o długości n do członu kombinatorycznego o długości Θ ( n ³ ).

Wyjaśnienie transformacji T [ ]

T [] transformacji motywowane chęci wyeliminowania abstrakcji. Dwa szczególne przypadki, reguły 3 i 4, są trywialne: λx . x jest wyraźnie równoważne I i λx . E jest wyraźnie równoważne ( K T [ E ]), jeżeli x nie wydaje się być wolny w E .

Pierwsze dwie reguły są również proste: zmienne konwertują do siebie, a aplikacje, które są dozwolone w kategoriach kombinacyjnych, są konwertowane na kombinatory po prostu przez konwersję applicand i argumentu na kombinatory.

Interesujące są zasady 5 i 6. Zasada 5 mówi po prostu, że aby przekonwertować złożoną abstrakcję na kombinator, musimy najpierw przekonwertować jej ciało na kombinator, a następnie wyeliminować abstrakcję. Zasada 6 faktycznie eliminuje abstrakcję.

λx .( E ₁ E ₂) jest funkcją, która przyjmuje argument, powiedzmy a , i podstawia go do wyrażenia lambda ( E ₁ E ₂ ) w miejsce x , co daje ( E ₁ E ₂ ) [ x  : = a ] . Ale podstawienie a na ( E ₁ E ₂) w miejsce x jest tym samym, co zastąpienie go zarówno E ₁ jak i E ₂, więc

( E ₁ E ₂)[ x  := a ] = ( E ₁ [ x  := a ] E ₂ [ x  := a ])

( λx .( E ₁ E ₂) a ) = (( λx . E ₁ a ) ( λx . E ₂ a ))

= ( S λx . E ₁ λx . E ₂ a )

= (( S λx . E₁ λx . E ₂) a )

Poprzez równość ekstensjonalną,

λx .( E ₁ E ₂) = ( S λx . E ₁ λx . E ₂)

Dlatego, aby znaleźć kombinator równoważny λx .( E ₁ E ₂), wystarczy znaleźć kombinator równoważny ( S λx . E ₁ λx . E ₂) i

( S T [ λx . E ₁] T [ λx . E ₂])

ewidentnie pasuje do rachunku. E ₁ i E ₂ zawierają ściśle mniej aplikacji niż ( E ₁ E ₂), więc rekurencja musi kończyć się wyrażeniem lambda bez żadnych aplikacji — albo zmienną, albo wyrażeniem w postaci λx . E .

Uproszczenia transformacji

η-redukcja

Kombinatory generowane przez transformację T [ ] można zmniejszyć, jeśli weźmiemy pod uwagę zasadę η-redukcji :

T [ λx .( E x )] = T [ E ] (jeśli x nie jest wolne w E )

λx .( E x) jest funkcją, która przyjmuje argument x i stosuje do niego funkcję E ; extensionally jest równa funkcji E siebie. Dlatego wystarczy przekonwertować E na formę kombinatoryjną.

Biorąc pod uwagę to uproszczenie, powyższy przykład staje się:

  T [ λx . λy .( y x )]

= ...

= ( S ( K ( SI )) T [ λx .( K x )])

= ( S ( K ( SI )) K ) (przez redukcję η)

Ten kombinator jest odpowiednikiem wcześniejszego, dłuższego:

  ( S ( K ( SI )) K x y )

= ( K ( SI ) x ( K x ) y )

= ( SI ( K x ) y )

= ( I Y ( K x Y ))

= ( Y ( K x Y ))

= ( yx )

Podobnie oryginalna wersja transformacji T [ ] przekształciła funkcję tożsamościową λf . λx . ( f x ) do ( S ( S ( KS ) ( S ( KK ), I )), ( KI )). Z zasadą η-redukcji, λf . λx .( f x ) przekształca się w I .

Jednopunktowa podstawa

Istnieją bazy jednopunktowe, z których każdy kombinator może być złożony ekstensywnie równym dowolnemu członowi lambda. Najprostszym przykładem takiej bazy jest { X } gdzie:

X ≡ λx .((x S ) K )

Nietrudno zweryfikować, że:

X ( X ( X X )) = ^β K i

X ( X ( X ( x X ))) = ^β S .

Ponieważ { K , S } jest bazą, wynika z tego, że { X } również jest bazą. Język programowania Iota używa X jako jedynego kombinatora.

Innym prostym przykładem podstawy jednopunktowej jest:

X' ≡ λx .(x K S K ) z

( X' X' ) X' = ^β K i

X' ( X' X' ) = ^β S

W rzeczywistości istnieje nieskończenie wiele takich baz.

Kombinatory B, C

Oprócz S i K , dokument Schönfinkela zawierał dwa kombinatory , które obecnie nazywają się B i C , z następującymi redukcjami:

( C f g x ) = (( f x ) g )

( B f g x ) = ( f ( g x ))

Wyjaśnia również, w jaki sposób można je z kolei wyrazić za pomocą tylko S i K :

B = ( S ( KS ) K )

C = ( S ( S ( K ( S ( KS ) K )) S ) ( KK ))

Te kombinatory są niezwykle przydatne podczas tłumaczenia logiki predykatów lub rachunku lambda na wyrażenia kombinatorowe. Wykorzystywał je również Curry , a znacznie później David Turner , którego nazwisko kojarzy się z ich obliczeniowym zastosowaniem. Za ich pomocą możemy rozszerzyć reguły transformacji w następujący sposób:

1. T [ x ] ⇒ x
2. T [( E₁ E₂ )] ⇒ ( T [ E₁ ] T [ E₂ ])
3. T [ λx . E ] ⇒ ( K T [ E ]) (jeśli x nie jest wolne w E )
4. T [ λx . x ] ⇒ I
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λ y . E ]] (jeśli x jest wolne w E )
6. T [ λx .( E₁ E₂ )] ⇒ ( S T [ λx . E₁ ] T [ λx . E₂ ]) (jeśli x jest wolne zarówno w E₁ jak i E₂ )
7. T [ λx .( E₁ E₂ )] ⇒ ( C T [ λx . E₁ ] T [ E₂ ]) (jeśli x jest wolne w E₁ ale nie E₂ )
8. T [ λx .( E₁ E₂ )] ⇒ ( B T [ E₁ ] T [ λx . E₂ ]) (jeśli x jest wolne w E₂ ale nie E₁ )

Używając kombinatorów B i C , przekształcenie λx . λy .( y x ) wygląda tak:

   T [ λx . λy .( y x )]

= T [ λx . T [ y . ( y x )]]

= T [ λx .( C T [ λy . y ] x )] (zgodnie z zasadą 7)

= T [ λx .( C I x )]

= ( C I ) (η-redukcja)

= (tradycyjny zapis kanoniczny : )${\ Displaystyle \ mathbf {C} _ {*}}$${\ Displaystyle \ mathbf {X} _ {*} = \ mathbf {XI}}$

= (tradycyjny zapis kanoniczny: )${\ Displaystyle \ mathbf {ja} '}$${\ Displaystyle \ mathbf {X} '= \ mathbf {CX}}$

I rzeczywiście, ( C I x y ) redukuje się do ( y x ):

   ( C I x R )

= ( I y x )

= ( y x )

Motywacją jest to, że B i C są ograniczonymi wersjami S . Podczas gdy S przyjmuje wartość i podstawia ją zarówno do aplikacji, jak i do jej argumentu przed wykonaniem aplikacji, C wykonuje podstawienie tylko w aplikacji, a B tylko w argumencie.

Współczesne nazwy kombinatorów pochodzą z pracy doktorskiej Haskella Curry'ego z 1930 r. (patrz B, C, K, W System ). W oryginalnej pracy Schönfinkela to, co teraz nazywamy S , K , I , B i C , nazywano odpowiednio S , C , I , Z i T .

Zmniejszenie rozmiaru kombinatora, które wynika z nowych reguł transformacji, można również osiągnąć bez wprowadzania B i C , jak pokazano w sekcji 3.2.

Rachunek CL _K kontra CL _I

Należy dokonać rozróżnienia między rachunkiem CL _K opisanym w tym artykule a rachunkiem CL _I. Rozróżnienie odpowiada rozróżnieniu między rachunkiem λ _K i λ _I. W przeciwieństwie do rachunku λ _K, rachunek λ _I ogranicza abstrakcje do:

λx . E gdzie x ma co najmniej jedno wolne wystąpienie w E .

W konsekwencji kombinator K nie występuje w rachunku λ _I ani w rachunku CL _I. Stałe CL _I to: I , B , C i S , które stanowią podstawę, z której można składać wszystkie terminy CL _I (równość modulo). Każdy wyraz λ _I można przekształcić w równy kombinator CL _I zgodnie z regułami podobnymi do przedstawionych powyżej dla konwersji wyrazów λ _K na kombinatory CL _K. Zobacz rozdział 9 w Barendregt (1984).

Odwrotna konwersja

Konwersja L [ ] z wyrazów kombinatorycznych na wyrazy lambda jest banalna:

L [ I ] = λx . x

L [ K ] = λx . λy . x

L [ C ] = λx . λy . λz . ( x oo r )

L [ B ] = λx . λy . λz . ( x ( y oo ))

L [ S ] = λx . λy . λz . ( x oo ( r oo ))

L [( E₁ E₂ )] = ( L [ E₁ ] L [ E₂ ])

Zauważ jednak, że ta transformacja nie jest odwrotną transformacją żadnej z wersji T [ ], które widzieliśmy.

Nierozstrzygalność rachunku kombinatorycznego

Postaci normalnej jakikolwiek okres kombinacyjne, w których złożone jest pierwotne, które występują, jeżeli w ogóle, nie są stosowane w dosyć argumenty są uproszczone. Nie można rozstrzygnąć, czy ogólny termin kombinacyjny ma postać normalną; czy dwa wyrażenia kombinacyjne są równoważne itd. Jest to równoważne nierozstrzygalności odpowiednich problemów dla członów lambda. Jednak bezpośredni dowód jest następujący:

Po pierwsze, termin

Ω = ( S I I ( S I I ))

nie ma normalnej postaci, ponieważ redukuje się do siebie po trzech krokach, w następujący sposób:

   ( S I I ( S I I ))

= ( ja ( S I I ) ( ja ( S I I )))

= ( S I I ( I ( S I I )))

= ( S I I ( S I I ))

i oczywiście żaden inny nakaz redukcji nie może skrócić wyrażenia.

Załóżmy teraz, że N jest kombinatorem do wykrywania form normalnych, takim, że

${\ Displaystyle (\ mathbf {N} \ x) = {\ zacząć {przypadki} \ mathbf {T} {\ tekst {jeśli}} x {\ tekst {ma normalną formę}} \ \ \ mathbf {F} ,{\text{ inaczej.}}\end{przypadki}}}$

(Gdzie T i C oznaczają konwencjonalne kodowania Church prawdziwego i przerobionych λx . Λy . X i λx . Λy . Y , przekształcony kombinatorycznej logiki. Wersje kombinatorycznych mieć T = K i K = ( K I ) ).

Teraz pozwól

Z = ( C ( C ( B N ( S I I )) Ω ) I )

teraz rozważmy termin ( S I I Z ). Czy ( S I I Z ) ma postać normalną? Robi to wtedy i tylko wtedy, gdy:

  ( S I I Z )

= ( JA Z ( JA Z ))

= ( Z ( I Z ))

= ( Z Z )

= ( C ( C ( B N ( S I I )) Ω ) I Z ) (definicja Z )

= ( C ( B N ( S I I )) Ω Z I )

= ( B N ( S I I ) Z Ω I )

= ( N ( S I I Z ) Ω I )

Teraz musimy zastosować N do ( S I I Z ). Albo ( S I I Z ) ma postać normalną, albo nie. Jeżeli to nie ma postaci normalnej, a następnie zmniejsza powyższe w następujący sposób:

  ( N ( S I I Z ) Ω I )

= ( K Ω I ) (definicja N )

= Ω

ale Ω ma nie mieć normalną formę, więc mamy sprzeczność. Ale jeśli ( S I I Z ) nie ma postaci normalnej, powyższe zmniejsza się w następujący sposób:

  ( N ( S I I Z ) Ω I )

= ( K I Ω I ) (definicja N )

= ( ja ja )

= I

co oznacza, że ​​formą normalną ( S I I Z ) jest po prostu ja , kolejna sprzeczność. Dlatego hipotetyczny kombinator N postaci normalnej nie może istnieć.

Analogiczny logika kombinatoryczna twierdzenia Rice'a mówi, że nie ma pełnego nietrywialnego predykatu. Orzeczenie jest syntezatora, że przy stosowaniu, powraca albo T lub F . Predykat N jest nietrywialna jeśli są dwa argumenty A i B , tak że N = T i N B = C . Kombinator N jest kompletny wtedy i tylko wtedy, gdy N M ma postać normalną dla każdego argumentu M . Analogia do twierdzenia Rice'a mówi wtedy, że każdy kompletny orzeczenie jest trywialny. Dowód tego twierdzenia jest dość prosty.

Dowód: Reductio ad absurdum. Załóżmy, że istnieje kompletny nietrywialny orzeczenie, powiedzmy N . Ponieważ N ma być nietrywialne, istnieją kombinatory A i B takie, że

( N A ) = T i

( N B ) = F .

Zdefiniuj NEGACJA ≡ λx .(jeśli ( N x ) to B inaczej A ) ≡ λx .(( N x ) B A )

Zdefiniuj ABSURDUM ≡ ( Y NEGACJA)

Twierdzenie o punkcie stałym daje: ABSURDUM = (NEGACJA ABSURDUM), for

ABSURDUM ≡ ( NEGACJA Y ) = (NEGACJA ( NEGACJA Y )) ≡ (NEGACJA ABSURDUM).

Ponieważ N ma być kompletne albo:

1. ( N ABSURDUM) = F lub
2. ( N ABSURDUM) = T

• Przypadek 1: F = ( N ABSURDUM) = N (NEGACJA ABSURDUM) = ( N A ) = T , sprzeczność.
• Przypadek 2: T = ( N ABSURDUM) = N (NEGACJA ABSURDUM) = ( N B ) = F , znowu sprzeczność.

Stąd ( N ABSURDUM) nie jest ani T ani F , co przeczy założeniu, że N byłoby zupełnym predykatem nietrywialnym. CO BYŁO DO OKAZANIA

Z tego twierdzenia o nierozstrzygalności wynika bezpośrednio, że nie ma pełnego predykatu, który mógłby odróżnić terminy mające postać normalną od terminów, które nie mają postaci normalnej. Z powyższego wynika również, że jest nie kompletna orzecznikiem, powiedzmy sobie równe, tak że:

(RÓWNE AB ) = T jeśli A = B i

(RÓWNE AB ) = F jeśli A ≠ B .

Gdyby istniało EQUAL, to dla wszystkich A , λx. (RÓWNE x A ) musiałoby być kompletnym predykatem nietrywialnym.

Aplikacje

Kompilacja języków funkcyjnych

David Turner wykorzystał swoje kombinatory do implementacji języka programowania SASL .

Kenneth E. Iverson użył prymitywów opartych na kombinatorach Curry'ego w swoim języku programowania J , następcy APL . Umożliwiło to to, co Iverson nazwał programowaniem milczącym , czyli programowaniem w wyrażeniach funkcjonalnych nie zawierających zmiennych, wraz z potężnymi narzędziami do pracy z takimi programami. Okazuje się, że programowanie milczące jest możliwe w dowolnym języku podobnym do APL z operatorami zdefiniowanymi przez użytkownika.

Logika

Curry-Howard izomorfizm zakłada połączenie między logiką i programowania: każdy dowód twierdzenia z logiki intuicjonistycznej odpowiada redukcji typie wyrażenia lambda i odwrotnie. Ponadto twierdzenia można identyfikować za pomocą sygnatur typów funkcji. W szczególności typowana logika kombinatoryczna odpowiada systemowi Hilberta w teorii dowodu .

W K i S złożone jest odpowiadają axioms

AK : A → ( B → A ),

JAK : ( A → ( B → C )) → (( A → B ) → ( A → C )),

a zastosowanie funkcji odpowiada zasadzie oderwania (modus ponens)

MP : z A i A → B wywnioskować B .

Rachunek składający się z AK , AS i MP jest kompletny dla implikacyjnego fragmentu logiki intuicjonistycznej, który można zobaczyć w następujący sposób. Rozważmy zbiór W wszystkich dedukcyjnie domkniętych zbiorów formuł, uporządkowanych przez włączenie . Następnie jest intuicjonistyczna rama Kripkego , a model w tej ramce definiujemy przez ${\ Displaystyle \ langle W \ podseteq \ rangle }$${\ Displaystyle \ Vdash}$

${\ Displaystyle X \ Vdash A \ jeśli A \ w X.}$

Definicja ta spełnia warunki spełnienia →: z jednej strony, jeśli , i jest takie, że i , to przez modus ponens. Z drugiej strony, jeśli , to przez twierdzenie o dedukcji , a więc domknięcie dedukcyjne jest elementem takim, że , , i . ${\ Displaystyle X \ Vdash A \ do B}$${\ Displaystyle Y \ w W}$${\ Displaystyle Y \ supseteq X}$${\ Displaystyle Y \ Vdash A}$${\ Displaystyle Y \ Vdash B}$${\ Displaystyle X \ nie \ Vdash A \ do B}$${\ Displaystyle X, A \ nie \ vdash B}$${\ Displaystyle X \ filiżanka \ {A \}}$${\ Displaystyle Y \ w W}$${\ Displaystyle Y \ supseteq X}$${\ Displaystyle Y \ Vdash A}$${\ Displaystyle Y \ nie \ Vdash B}$

Niech A będzie dowolną formułą, której nie można udowodnić w rachunku różniczkowym. Wtedy A nie należy do dedukcyjnego domknięcia X zbioru pustego, a zatem , a A nie jest intuicjonistycznie poprawne. ${\ Displaystyle X \ nie \ Vdash A}$

Zobacz też

• Aplikacyjne systemy obliczeniowe
• Układ B, C, K, W
• Kategoryczna maszyna abstrakcyjna
• Kombinacyjna gramatyka kategorialna
• Wyraźna substytucja
• Kombinator punktów stałych
• Maszyna do redukcji wykresów
• Rachunek lambda i algebra cylindryczna , inne podejścia do modelowania ilościowego i eliminowania zmiennych
• Rachunek kombinatora SKI
• Superkombinator
• Wyśmiewać się z przedrzeźniacza

Bibliografia

Dalsza lektura

• Barendregt, Hendrik Pieter (1984). Rachunek lambda, jego składnia i semantyka. Studia z logiki i podstaw matematyki . Tom 103. Holandia Północna . Numer ISBN 0-444-87508-5. |volume=ma dodatkowy tekst ( pomoc )
• Curry, Haskell B .; Feys, Robert (1958). Logika kombinatoryczna . Tom. I. Amsterdam: Holandia Północna. Numer ISBN 0-7204-2208-6. |volume=ma dodatkowy tekst ( pomoc )
• Curry, Haskell B .; Hindley, J. Roger ; Seldin, Jonathan P. (1972). Logika kombinatoryczna . Tom. II. Amsterdam: Holandia Północna. Numer ISBN 0-7204-2208-6. |volume=ma dodatkowy tekst ( pomoc )
• Pole, Anthony J.; Harrison, Peter G. (1998). Programowanie funkcjonalne . Addisona-Wesleya. Numer ISBN 0-201-19249-7.
• Hindley, J. Roger ; Meredith, David (1990), "Główne schematy typu i skrócone oderwanie" , Journal of Symbolic Logic , 55 (1): 90-105, doi : 10.2307/2274956 , JSTOR  2274956 , MR  1043546
• Hindley, JR ; Seldin, JP (2008). Rachunek λ i kombinatory: wprowadzenie . Wydawnictwo Uniwersytetu Cambridge .
• Paulson, Lawrence C. (1995). Podstawy programowania funkcjonalnego . Uniwersytet Cambridge.
• Quine, WV (1960). „Zmienne wyjaśnione”. Materiały Amerykańskiego Towarzystwa Filozoficznego . 104 (3): 343-347. JSTOR  985250 .Przedrukowany jako rozdział 23 z Selected Logic Papers Quine'a (1966), s. 227-235
• Schönfinkel, Moses , 1924, „ Über die Bausteine ​​der mathematischen Logik ”, przetłumaczony jako „O klockach logiki matematycznej” w From Frege to Gödel: książka źródłowa w logice matematycznej, 1879-1931 , Jean van Heijenoort , wyd. Harvard University Press , 1967. ISBN  0-674-32449-8 . Artykuł, który założył logikę kombinatoryczną.
• Smullyan, Raymond , 1985. Wyśmiewać drozda . Knopf. ISBN  0-394-53491-3 . Łagodne wprowadzenie do logiki kombinatorycznej, przedstawione jako seria rekreacyjnych zagadek wykorzystujących metafory obserwacji ptaków.
• ______, 1994. Diagonalizacja i samoodniesienie . Wydawnictwo Uniwersytetu Oksfordzkiego . Rozdziały 17-20 są bardziej formalnym wprowadzeniem do logiki kombinatorycznej, ze szczególnym naciskiem na wyniki stałoprzecinkowe.
• Sørensen, Morten Heine B. i Paweł Urzyczyn, 1999. Wykłady na temat izomorfizmu Curry-Howarda . Uniwersytet Kopenhaski i Uniwersytet Warszawski , 1999.
• Wolfengagen, VE (2003). Logika kombinatoryczna w programowaniu: Obliczenia na obiektach poprzez przykłady i ćwiczenia (wyd. 2). Moskwa: „Centrum JurInfoR” Ltd. ISBN 5-89158-101-9.
• Wolfram, Stephen (2021). Kombinatory: widok stulecia . Wolfram Media . Numer ISBN 978-1-57955-043-1.e ISBN  978-1-57955-044-8 . Święto rozwoju kombinatorów sto lat po ich wprowadzeniu przez Mosesa Schönfinkela w 1920 roku.

Zewnętrzne linki

• Stanford Encyclopedia of Philosophy : „ Logika kombinacyjna ” Katalin Bimbó .
• 1920–1931 Notatki Curry'ego.
• Keenan, David C. (2001) „ Przeanalizować drozda: graficzna notacja dla rachunku lambda z animowaną redukcją ”.
• Rathman, Chris, „ Ptaki kombinatora ”. Stół, w którym destyluje większość istoty Smullyana (1985).
• Kombinatory przeciągnij i upuść. (Aplet Javy)
• Binarny rachunek lambda i logika kombinacyjna.
• Serwer sieciowy z redukcją logiki kombinacyjnej