Czysty rachunek Lambda - i funkcja

Question

Obecnie uczę się Haskella, a także uczestniczę w raczej teoretycznym wykładzie na temat programowania funkcjonalnego na uniwersytecie.

Wiem, że to jest czysto teoretyczne/akademickie pytanie, ale mimo to jestem zainteresowany, jak wyrażać różne proste funkcje po prostu z czystym rachunkiem lambda (to znaczy bez zdefiniowanych żadnych stałych).

Niektóre materiały wykład kopalni określają wartości logicznych, takich jak:

prawdziwego = \ xy.x
Fałsz = \ xy.y

(\ denotowania symbol lambda)

Jeśli są zdefiniowane tak jak te funkcje selektora, to if-con datkowe można łatwo zdefiniowany jako:

Jeśli = \ x.x

Teraz staram się wymyślić jakiś krótki formularz na logiczne „i” -function. Moje pierwsze przypuszczenie.

i = \ xy {(If x) [(Jeśli y) prawdaFałsz] Fałsz}

Tak zasadniczo ta funkcja lambda otrzyma 2 argumenty uv, gdzie oba muszą być wpisane jak True/False. Jeśli wykonuję różne redukcje beta ze wszystkimi czterema kombinacjami tabeli logicznej, otrzymuję właściwy wynik.

Mimo to ta funkcja wygląda trochę brzydko i myślę o nadaniu jej bardziej eleganckiego charakteru. Wszelkie propozycje tutaj?

Answer 1

Możemy po prostu obniżyć twoją odpowiedź, aby uzyskać bardziej zdecydowaną.

Najpierw kilka rozgrzewek. Oczywiście IF x ==> x, i jako TRUE TRUE FALSE ==> TRUE i FALSE TRUE FALSE ==> FALSE jeśli x jest boolowskie, to następnie x TRUE FALSE ==> x.

Teraz możemy zmniejszyć

\x y . (IF x) ((IF y) TRUE FALSE) FALSE 
\x y .  x ( y TRUE FALSE) FALSE -- using IF x   ==> x 
\x y .  x ( y   ) FALSE -- using y TRUE FALSE ==> y 
\x y . x y FALSE       -- clean up 

i to wyrażenie nadal współpracuje z tablica prawdy

AND TRUE TRUE = TRUE TRUE FALSE = TRUE 
AND FALSE TRUE = FALSE TRUE FALSE = FALSE 
AND TRUE FALSE = TRUE FALSE FALSE = FALSE 
AND FALSE FALSE = FALSE FALSE FALSE = FALSE 

Answer 2

Cóż, and True to funkcja identyfikacji, a and False to stała funkcja zwracająca False, więc możemy z niej korzystać.

and = \x. if x id (const False) 

który ma ładny symetrię

or = \x. if x (const True) id 

(gdzie

id = \x. x 
const = \x y. x 

)

Wspólny wzór eliminatory pobiera dane na końcu listy argumentów, które często działa elegancko w stylu pointfree, więc jeśli zdefiniowałeś:

cond = \t f b. b t f 

następnie można wyrazić

and = cond id (const False) 
or = cond (const True) id 

który jest najlepszy mam. Prawdopodobnie są jeszcze bardziej eleganckie formuły, oglądając bool w fajny sposób.

Answer 3

booleans Kościoła, prawda? :) Opracowałem dla zabawy mały moduł za pomocą funkcji RankNTypes, aby przedstawić je jak najbliżej oryginalnej wersji rachunku lambda.

Tak więc, jeśli pozwalają RankNTypes:

{-# LANGUAGE RankNTypes #-} 

Możecie reprezentować typ logicznych Kościoła jako funkcji a -> a -> a dla każdego typu a, więc o zwartej reprezentacji Prawda i fałsz bardzo podobny do Ciebie. Wpisanie tutaj pozwoli nam swobodniej komponować funkcje.

type CBool = forall a. a -> a -> a 

ctrue :: CBool 
ctrue t f = t 

cfalse :: CBool 
cfalse t f = f 

Teraz, jak jest koniunkcja napisana w tych kategoriach? Załóżmy, że masz lewy operand l i prawy operand r, które są zarówno CBool, czyli funkcje a -> a -> a, które zwracają ci pierwszy lub drugi parametr w zależności od tego, czy jest to ctrue czy cfalse. Możesz ocenić tę funkcję, podając jako dane wejściowe r i jako trzecią jako l. Jeśli l jest ctrue, to oceni swój pierwszy parametr, który jest r: znowu powinien być ctrue, wtedy nasza spójność jest spełniona. W każdym innym przypadku zostanie zwrócone: cfalse.

cand :: CBool -> CBool -> CBool 
cand l r = l r l 

alternatywą może być reprezentowany w sposób podobny z tym samym chwytem bezpośredniego oszacowania funkcji reprezentującymi wartości logiczne zawartych w wejściowych.Tyle że tutaj będziesz zamienić dwa argumenty do oceny l: jeśli l jest ctrue, powróci sama l inaczej to wszystko do r wartość powinna

cor :: CBool -> CBool -> CBool 
cor l r = l l r 

Włączając RankNTypes, myślę, że jest to najbliżej, jak można uzyskać pierwotne definicje koniunkcji i rozłączności dla liczb boolowskich Kościoła w Rachunku Lambda. Napisałem również funkcje do tłumaczenia z regularnych Bool i CBool, negacji, a także naturalnych liczb Kościoła w tym samym stylu. Cały kod źródłowy można znaleźć pod adresem https://github.com/rtraverso86/haskkit/blob/master/Haskkit/Data/Church.hs.