Rachunek kombinacyjny SKI

Rachunek kombinatorowy SKI to kombinatoryczny system logiczny i system obliczeniowy . Można go traktować jako język programowania komputerowego, chociaż nie jest wygodny do pisania oprogramowania. Zamiast tego jest ważny w matematycznej teorii algorytmów, ponieważ jest to niezwykle prosty kompletny język Turinga . Można go porównać do zredukowanej wersji rachunku lambda bez typu . Wprowadzili go Moses Schönfinkel i Haskell Curry .

Wszystkie operacje w rachunku lambda można zakodować poprzez eliminację abstrakcji do rachunku SKI jako drzewa binarne , których liście są jednym z trzech symboli S , K i I (zwanych kombinatorami ).

Notacja

Chociaż najbardziej formalna reprezentacja obiektów w tym systemie wymaga drzew binarnych, dla uproszczenia składu są one często reprezentowane jako wyrażenia w nawiasach, jako skrót drzewa, które reprezentują. Wszelkie poddrzewa mogą być ujęte w nawiasy, ale często tylko poddrzewa po prawej stronie są ujęte w nawiasy, z lewą asocjatywnością implikowaną dla wszelkich aplikacji bez nawiasów. Na przykład ISK oznacza (( IS ) K ). Korzystając z tej notacji, drzewo, którego lewym poddrzewem jest drzewo KS , a prawym poddrzewem jest drzewo SK , można zapisać jako KS ( SK ). Jeśli pożądana jest większa jednoznaczność, można również dołączyć domniemane nawiasy: (( KS )( SK )).

Nieformalny opis

Nieformalnie, używając żargonu języka programowania, drzewo ( xy ) można traktować jako funkcję x zastosowaną do argumentu y . Podczas oceny ( tj . gdy funkcja jest „zastosowana” do argumentu), drzewo „zwraca wartość”, tj . przekształca się w inne drzewo. „Funkcja”, „argument” i „wartość” są albo kombinatorami, albo drzewami binarnymi. Jeśli są to drzewa binarne, w razie potrzeby można je również traktować jako funkcje.

Operacja oceny jest zdefiniowana w następujący sposób:

( x , y i z reprezentują wyrażenia utworzone z funkcji S , K i I oraz ustawiają wartości):

Zwracam jego argument:

ja x = x

K zastosowane do dowolnego argumentu x daje jednoargumentową stałą funkcję K x , która zastosowana do dowolnego argumentu zwraca x :

Kxy = x _

S jest operatorem podstawienia. Pobiera trzy argumenty, a następnie zwraca pierwszy argument zastosowany do trzeciego, który jest następnie stosowany do wyniku drugiego argumentu zastosowanego do trzeciego. Jaśniej:

S xyz = xz ( yz )

Przykładowe obliczenie: SKSK oblicza KK ( SK ) według reguły S. Następnie, jeśli obliczymy KK ( SK ), otrzymamy K na podstawie K -reguły. Ponieważ nie można zastosować żadnej innej reguły, obliczenia zatrzymują się w tym miejscu.

Dla wszystkich drzew x i wszystkich drzew y , SK xy będzie zawsze oceniane na y w dwóch krokach, K y ( xy ) = y , więc ostateczny wynik obliczania SK xy będzie zawsze równy wynikowi obliczania y . Mówimy, że SK x i I są „funkcjonalnie równoważne”, ponieważ zawsze dają ten sam wynik po zastosowaniu do dowolnego y .

Na podstawie tych definicji można wykazać, że rachunek SKI nie jest systemem minimalnym, który może w pełni wykonać obliczenia rachunku lambda, ponieważ wszystkie wystąpienia I w dowolnym wyrażeniu można zastąpić przez ( SKK ) lub ( SKS ) lub ( SK cokolwiek) i wynikowe wyrażenie da ten sam wynik. Zatem „ ja ” jest jedynie cukrem składniowym . Ponieważ I jest opcjonalny, system jest również nazywany rachunkiem różniczkowym SK lub rachunkiem kombinowanym SK.

Możliwe jest zdefiniowanie kompletnego systemu za pomocą tylko jednego (niewłaściwego) kombinatora. Przykładem jest jota Chrisa Barkera , który można wyrazić za pomocą S i K w następujący sposób:

ι x = x SK

Możliwe jest zrekonstruowanie S , K i I z kombinatora jota. Zastosowanie ι do samego siebie daje ιι = ι SK = SSKK = SK ( KK ) co jest funkcjonalnie równoważne I . K można skonstruować, stosując dwukrotnie ι do I (co jest równoważne z zastosowaniem ι do samego siebie): ι(ι(ιι)) = ι(ιι SK ) = ι( ISK ) = ι( SK ) = SKSK = K . Zastosowanie ι jeszcze raz daje ι(ι(ι(ιι))) = ι K = KSK = S .

Definicja formalna

Terminy i pochodne w tym systemie można również zdefiniować bardziej formalnie:

Terminy : zbiór T terminów jest definiowany rekurencyjnie według następujących reguł.

  1. S , K i I są wyrazami.
  2. Jeśli τ 1 i τ 2 są wyrazami, to (τ 1 τ 2 ) jest wyrazem.
  3. Nic nie jest terminem, jeśli nie jest wymagane przez dwie pierwsze zasady.

Derywacje : Derywacja to skończona sekwencja terminów zdefiniowanych rekurencyjnie według następujących reguł (gdzie α i ι to słowa nad alfabetem { S , K , I , (, )}, podczas gdy β, γ i δ to wyrazy):

  1. Jeśli Δ jest wyprowadzeniem kończącym się wyrażeniem postaci α( I β)ι, to Δ, po którym następuje wyraz αβι, jest pochodną.
  2. Jeśli Δ jest wyprowadzeniem zakończonym wyrażeniem w postaci α(( K β)γ)ι, to Δ, po którym następuje wyraz αβι, jest pochodną.
  3. Jeśli Δ jest wyprowadzeniem zakończonym wyrażeniem w postaci α((( S β)γ)δ)ι, to Δ, po którym następuje wyraz α((βδ)(γδ))ι, jest pochodną.

Zakładając, że sekwencja jest prawidłowym wyprowadzeniem, można ją rozszerzyć za pomocą tych reguł. Wszystkie wyprowadzenia o długości 1 są poprawnymi wyprowadzeniami.

Rekurencyjne przekazywanie i cytowanie parametrów

K=λq.λi.q
cytuje q i ignoruje i
S=λx.λy.λz.((xz)(yz))
tworzy drzewo binarne, którego parametry mogą przepływać od korzenia do gałęzi i być odczytywane przez identityFunc=((SK) K) lub przeczytaj cytowaną lambda q używając Kq.

wyrażenia narciarskie

Samodzielna aplikacja i rekurencja

SII to wyrażenie, które pobiera argument i stosuje go do siebie:

SII α = ja α( ja α) = αα

Jest to znane jako kombinator U. Jedną z jego interesujących właściwości jest to, że jego samozastosowanie jest nieredukowalne:

SII ( SII ) = ja ( SII ) ( ja ( SII )) = SII ( ja ( SII )) = SII ( SII )

Inną rzeczą jest to, że pozwala napisać funkcję, która stosuje jedną rzecz do samodzielnego zastosowania innej rzeczy:

( S ( K α)( SII ))β = K αβ( SII β) = α( ja β( ja β)) = α(ββ)

Tej funkcji można użyć do osiągnięcia rekurencji . Jeśli β jest funkcją, która stosuje α do samodzielnego zastosowania czegoś innego,

β = S ( K α) ( SII )

wtedy samozastosowanie tego β jest punktem stałym tego α:

SII β = β β = α (β β) = α (α (β β)) =

Jeśli α wyraża „krok obliczeniowy” obliczony przez αρν dla pewnych ρ i ν, co zakłada, że ​​ρν' wyraża „resztę obliczeń” (dla niektórych ν', które α „obliczy” z ν), wówczas jego punkt stały ββ wyraża całe obliczenie rekurencyjne, ponieważ użycie tej samej funkcji ββ dla wywołania „reszty obliczeń” (z ββν = α(ββ)ν) jest samą definicją rekurencji: ρν' = ββν' = α(ββ)ν' = . .. . α będzie musiał zastosować jakiś tryb warunkowy, aby zatrzymać się na jakimś „przykładzie podstawowym” i nie wykonywać wtedy wywołania rekurencyjnego, aby uniknąć rozbieżności.

Można to sformalizować, np

β = H α = S ( K α)( SII ) = S ( KS ) K α ( SII ) = S ( S ( KS ) K ) ( K ( SII )) α

Jak

Y α = SII β = SII ( H α) = S ( K ( SII )) H α = S ( K ( SII ))( S ( S ( KS ) K ) ( K ( SII ))) α

co daje nam jedno możliwe kodowanie kombinatora Y.

Wyrażenie odwrotne

S ( K ( SI )) K odwraca następujące dwa wyrazy:

S ( K ( SI )) K αβ →
K ( SI ) α ( K α) β →
SI ( K α) β →
ja β ( K αβ) →
ja βα →
βα

Logika boolowska

Rachunek kombinacyjny SKI może również implementować logikę Boole'a w postaci struktury if-then-else . Struktura if-then-else składa się z wyrażenia boolowskiego, które może być prawdziwe ( T ) lub fałszywe ( F ) oraz dwóch argumentów, takich jak:

Txy = x _

I

Fxy = y _

Kluczem jest zdefiniowanie dwóch wyrażeń boolowskich. Pierwszy działa podobnie jak jeden z naszych podstawowych kombinatorów:

T = K
K xy = x

Drugi jest również dość prosty:

F = SK
SK xy = K y(xy) = y

Po zdefiniowaniu prawdy i fałszu cała logika boolowska może zostać zaimplementowana w kategoriach struktur if-then-else .

Boolean NOT (która zwraca przeciwieństwo danej wartości logicznej) działa tak samo jak struktura if-then-else , z F i T jako drugą i trzecią wartością, więc może być zaimplementowana jako operacja przyrostkowa:

NIE = ( fa ) ( T ) = ( SK ) ( K )

Jeśli umieścimy to w strukturze if-then-else , można wykazać, że ma to oczekiwany wynik

( T ) NIE = T ( fa ) ( T ) = fa
( fa ) NIE = fa ( fa ) ( T ) = T

Boolean OR (która zwraca T , jeśli jedną z dwóch otaczających ją wartości boolowskich jest T ) działa tak samo jak struktura if-then-else z T jako drugą wartością, więc może być zaimplementowana jako operacja infiksowa:

LUB = T = K

Jeśli umieścimy to w strukturze if-then-else , można wykazać, że ma to oczekiwany wynik:

( T ) LUB ( T ) = T ( T ) ( T ) = T
( T ) LUB ( fa ) = T ( T ) ( fa ) = T
( fa ) LUB ( T ) = fa ( T ) ( T ) = T
( fa ) LUB ( fa ) = fa ( T )( fa ) = fa

Boolean AND (który zwraca T , jeśli obie otaczające go wartości logiczne to T ) działa tak samo jak struktura if-then-else z F jako trzecią wartością, więc może być zaimplementowana jako operacja przyrostkowa:

AND = F = SK

Jeśli umieścimy to w strukturze if-then-else , można wykazać, że ma to oczekiwany wynik:

( T ) ( T ) I = T ( T ) ( fa ) = T
( T ) ( fa ) I = T ( fa ) ( fa ) = fa
( fa ) ( T ) I = fa ( T ) ( fa ) = fa
( fa ) ( fa ) I = fa ( fa )( fa ) = fa

Ponieważ definiuje to T , F , NOT (jako operator przyrostkowy), OR (jako operator infiksowy) i AND (jako operator przyrostkowy) w kategoriach notacji SKI, dowodzi to, że system SKI może w pełni wyrazić logikę boolowską.

Ponieważ rachunek SKI jest kompletny , możliwe jest również wyrażenie NOT , OR i AND jako operatorów przedrostkowych:

NIE = S ( SI ( KF ))( KT ) (jako S ( SI ( KF ))( KT ) x = SI ( KF ) x ( KT x ) = ja x ( KF x ) T = x FT )
LUB = SI ( KT ) (jako SI ( KT ) xy = ja x ( KT x ) y = x T y )
AND = SS ( K ( KF )) (jako SS ( K ( KF )) xy = S x ( K ( KF ) x ) y = xy ( KF y ) = xy fa )

Połączenie z logiką intuicjonistyczną

Kombinatory K i S odpowiadają dwóm dobrze znanym aksjomatom logiki zdaniowej :

AK : ZA → ( b → ZA ) ,
AS : ( ZA → ( b → do )) → (( ZA → b ) → ( ZA → do )) .

Zastosowanie funkcji odpowiada zasadzie modus ponens :

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

Aksjomaty AK i AS oraz reguła MP są kompletne dla implikacyjnego fragmentu logiki intuicjonistycznej . Aby logika kombinacyjna miała za wzór:

To połączenie między typami kombinatorów i odpowiadającymi im aksjomatami logicznymi jest przykładem izomorfizmu Curry'ego – Howarda .

Przykłady redukcji

Sposobów na redukcję może być wiele. Wszystkie są równoważne, o ile nie złamiesz kolejności operacji

Zobacz też

  •   Smullyan, Raymond (1985). Wyśmiać drozda . Knopf. ISBN 0-394-53491-3 . Delikatne wprowadzenie do logiki kombinatorycznej, przedstawione jako seria rekreacyjnych łamigłówek wykorzystujących metafory obserwacji ptaków.
  •    — (1994). „Rozdz. 17–20”. Diagonalizacja i samoodniesienie . Oxford University Press. ISBN 9780198534501 . OCLC 473553893 . są bardziej formalnym wprowadzeniem do logiki kombinatorycznej, ze szczególnym naciskiem na wyniki punktów stałych.

Linki zewnętrzne

Pobrano z „ https://en.wikipedia.org/w/index.php?title=SKI_combinator_calculus&oldid=1141781681 ”