Konwertuj wyrażenia λ na wyrażenia SK

Λ-rachunek lub rachunek lambda, to system logiczny na podstawie funkcji anonimowych. Na przykład jest to wyrażenie λ:

λf.(λx.xx)(λx.f(xx))

Jednak na potrzeby tego wyzwania uprościmy notację:

• Zmień λna \(aby ułatwić pisanie):\f.(\x.xx)(\x.f(xx))
• .W nagłówkach lambda jest niepotrzebny, więc możemy go upuścić:\f(\xxx)(\xf(xx))
• Użyj notacji prefiksowej w stylu Unlambda z `do aplikacji zamiast pisać dwie funkcje razem (aby uzyskać pełne wyjaśnienie, jak to zrobić, zobacz Konwersja między notacjami Lambda Calculus ):\f`\x`xx\x`f`xx
• To najbardziej skomplikowana zamiana. Zastąp każdą zmienną liczbą w nawiasach, zależnie od tego, jak głęboko zagnieżdżona jest zmienna względem nagłówka lambda, do którego należy (tj. Użyj indeksowania De Bruijn opartego na 0 ). Na przykład w \xx(funkcja tożsamości) xtreść zostanie zastąpiona przez [0], ponieważ należy ona do pierwszego (opartego na 0) nagłówka napotkanego podczas przechodzenia do wyrażenia od zmiennej do końca; \x\y``\x`xxxyzostanie zamieniony na \x\y``\x`[0][0][1][0]. Możemy teraz upuścić zmienne w nagłówkach, pozostawiając \\``\`[0][0][1][0].

Logika kombinacyjna to w zasadzie Tarpit Turinga wykonany z rachunku λ (właściwie to był pierwszy, ale tutaj nie ma to znaczenia).

„Logikę kombinacyjną można postrzegać jako wariant rachunku lambda, w którym wyrażenia lambda (reprezentujące abstrakcję funkcjonalną) są zastępowane ograniczonym zestawem kombinatorów, prymitywnych funkcji, w których nie ma powiązanych zmiennych.” ¹

Najczęstszym rodzajem logiki kombinatorycznej jest rachunek kombinatoryczny SK , który wykorzystuje następujące operacje podstawowe:

K = λx.λy.x
S = λx.λy.λz.xz(yz)

Czasami I = λx.xdodawany jest kombinator , ale jest on zbędny, ponieważ SKK(lub SKxdla dowolnego x) jest równoważny I.

Wszystko czego potrzebujesz to K, S i aplikacja, aby móc zakodować dowolne wyrażenie w rachunku λ. Jako przykład, oto tłumaczenie z funkcji λf.(λx.xx)(λx.f(xx))na logikę kombinacyjną:

λf.(λx.xx)(λx.f(xx)) = S(K(λx.xx))(λf.λx.f(xx))
λx.f(xx) = S(Kf)(S(SKK)(SKK))
λf.λx.f(xx) = λf.S(Kf)(S(SKK)(SKK))
λf.S(Sf)(S(SKK)(SKK)) = S(λf.S(Sf))(K(S(SKK)(SKK)))
λf.S(Sf) = S(KS)S
λf.λx.f(xx) = S(S(KS)S)(K(S(SKK)(SKK)))
λx.xx = S(SKK)(SKK)
λf.(λx.xx)(λx.f(xx)) = S(K(S(SKK)(SKK)))(S(S(KS)S)(K(S(SKK)(SKK))))

Ponieważ używamy notacji przedrostkowej, tak jest ```S`K``S``SKK``SKK``S``S`KSS`K``SKK`.

_{¹ Źródło: Wikipedia}

Wyzwanie

Do tej pory prawdopodobnie zgadłeś, co to jest: Napisz program, który przyjmuje poprawne wyrażenie λ (w opisie powyżej opisanym) jako dane wejściowe i wyjściowe (lub zwraca) tę samą funkcję, przepisaną w rachunku SK-kombinatory. Zauważ, że istnieje nieskończona liczba sposobów na przepisanie tego; potrzebujesz tylko jednego z nieskończonych sposobów.

To jest golf golfowy , więc wygrywa najkrótsze prawidłowe zgłoszenie (mierzone w bajtach).

Przypadki testowe

Każdy przypadek testowy pokazuje jedno możliwe wyjście. Wyrażenie na górze jest równoważnym wyrażeniem rachunku λ.

λx.x:
\[0]                        -> ``SKK
λx.xx:
\`[0][0]                    -> ```SKK``SKK
λx.λy.y:
\\[0]                       -> `SK
λx.λy.x:
\\[1]                       -> K
λx.λy.λz.xz(yz):
\\\``[2][0]`[1][0]          -> S
λw.w(λx.λy.λz.xz(yz))(λx.λy.x):
\``[0]\\[1]\\\``[2][0]`[1][0] -> ``S``SI`KS`KK

Haskell, 251 237 222 214 bajtów

15 bajtów zapisanych dzięki @ Ørjan_Johansen (zobacz także jego linki TIO w uwagach)!

8 bajtów więcej zapisanych dzięki @nimi!

data E=S|K|E:>E|V Int
p(h:s)|h>'_',(u,a)<-p s,(v,b)<-p u=(v,a:>b)|h>'['=a<$>p s|[(n,_:t)]<-reads s=(t,V n)
a(e:>f)=S:>a e:>a f
a(V 0)=S:>K:>K
a(V n)=K:>V(n-1)
a x=K:>x
o(e:>f)='`':o e++o f
o S="S"
o K="K"
f=o.snd.p

panalizuje dane wejściowe, zwracając pozostałą niepodzieloną część w pierwszym składniku wynikowej pary. Pierwszym znakiem argumentu musi być lewy ukośnik, odwrotny ukośnik lub nawias otwierający. Strażnicy wzorów psprawdzają te przypadki w tej kolejności. W pierwszym przypadku, oznaczającym aplikację, dwa kolejne wyrażenia są analizowane i łączone z elementem Etypu danych za pomocą konstruktora infix :>. W przypadku lambda następujące wyrażenie jest analizowane i natychmiast przekazywane do afunkcji. W przeciwnym razie jest to zmienna, otrzymujemy jej liczbę za pomocą readsfunkcji (która zwraca listę) i upuszczamy nawias zamykający, dopasowując wzór (_:t).

aFunkcja robi dość dobrze znany wspornik abstrakcję. Aby wyodrębnić aplikację, wyodrębniamy dwa podwyrażenia i używamy Skombinatora do rozdzielenia argumentu na oba. Jest to zawsze poprawne, ale przy większej ilości kodu moglibyśmy zrobić znacznie więcej , zajmując się specjalnymi przypadkami w celu uzyskania krótszych wyrażeń. Abstrahując aktualną zmienną daje Ilub, gdy nie mamy, że SKK. Zwykle pozostałe przypadki mogą po prostu dodać a Kz przodu, ale używając tej notacji musimy zmienić numerację zmiennych, ponieważ wewnętrzna lambda jest abstrakcyjna.

ozamienia wynik na ciąg wyjściowy. fjest pełną funkcją.

Podobnie jak w wielu językach, odwrotny ukośnik jest znakiem ucieczki, dlatego musi być podany dwukrotnie w dosłownym ciągu:

*Main> f "\\[0]"
"``SKK"
*Main> f "\\`[0][0]"
"``S``SKK``SKK"
*Main> f "\\\\[0]"
"``S``S`KS`KK`KK"
*Main> f "\\\\[1]"
"``S`KK``SKK"
*Main> f "\\\\\\``[2][0]`[1][0]"
"``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S`KK`KK``S`KK``SKK``S``S`KS``S``S`KS``S`KK`KS``S`KK`KK``S`KK`KK``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S`KK`KK``S``S`KS`KK`KK``S``S`KS``S``S`KS``S`KK`KS``S`KK`KK``S`KK`KK"