Lambda Calculus Generator

10

Nie wiem, gdzie jeszcze zadać to pytanie, mam nadzieję, że to dobre miejsce.

Jestem tylko ciekawy, czy można zrobić generator lambda; zasadniczo pętla, która w nieskończonym czasie wytworzy każdą możliwą funkcję rachunku lambda. (jak w postaci ciągu).

Ponieważ rachunek lambda jest tak prosty, mając tylko kilka elementów do jego zapisu, pomyślałem, że może być możliwe (choć niezbyt przydatne) utworzenie wszystkich możliwych kombinacji tych elementów zapisu, zaczynając od najprostszych kombinacji, a tym samym wytworzenie każdej możliwej lambda funkcja rachunku różniczkowego.

Oczywiście nie wiem prawie nic o rachunku lambda, więc nie mam pojęcia, czy to naprawdę możliwe.

Czy to jest Jeśli tak, to czy jest to tak proste, jak to sobie wyobrażałem, czy jest to technicznie możliwe, ale tak trudne, że jest faktycznie niemożliwe?

PS. Nie mówię o funkcjach obniżonych beta, mówię tylko o każdej poprawnej notacji każdej funkcji rachunku lambda.

Legit Stack
źródło

Odpowiedzi:

19

Jasne, to standardowe ćwiczenie kodowania.

Przede wszystkim niech dowolna dwuskładnikowa funkcja obliczeniowa, zwana funkcją parowania. Standardowym wyborem jestp:N2N

p(n,m)=(n+m)(n+m+1)2+n

Można udowodnić, że jest to bijectcja, więc biorąc pod uwagę każdy naturalny , możemy obliczyć n , m tak, że p ( n , m ) = k .kn,mp(n,m)=k

Aby wyliczyć terminy lambda, popraw dowolne wyliczenie dla nazw zmiennych: .x0,x1,x2,

Następnie dla każdej liczby naturalnej wydrukuj l a m b d a ( i ) , zdefiniowane rekurencyjnie w następujący sposób:ilambda(i)

  • jeśli jest parzyste, niech j = i / 2 i zwróci zmienną x jij=i/2xj
  • jeśli jest nieparzyste, niech j = ( i - 1 ) / 2ij=(i1)/2
    • jk=j/2n,mp(n,m)=kN=lambda(n),M=lambda(m)(NM)
    • jk=(j1)/2n,mp(n,m)=kM=lambda(m)(λxn. M)

Λ

ΛN+(Λ2+N×Λ)

które jest odczytywane jako „składowe lambda, składniowo, są rozłącznym połączeniem 1) zmiennych (przedstawionych jako naturalne), 2) aplikacji (wykonanych przez dwa terminy lambda) oraz 3) abstrakcji (para zmienna / naturalny + termin lambda ) ”.

N2NpN+NN

Ta procedura jest ogólna i działa na prawie każdym języku generowanym przez gramatykę bezkontekstową, która zapewni podobny izomorfizm do powyższego.

chi
źródło
Wow, dziękuję, czy to możliwe, że możesz reprezentować ten pseudo kod? Zdecydowanie lepiej to zrozumiem, ponieważ nie mam dyplomu cs.
Legit Stack
3
lambda(n)if n%2==0 ...n,mp(n,m)=kn,mn,mk
1
a=12(8k+11),b=12a(a+1),n=bk,m=an
12

Tak. Weź coś, co wylicza wszystkie możliwe ciągi ASCII. Dla każdego wyjścia sprawdź, czy jest to poprawna składnia rachunku lambda, która definiuje funkcję; jeśli nie, pomiń to. (Można to sprawdzić.) Wymienia wszystkie funkcje rachunku lambda.

DW
źródło
5
Zasadniczo wszystkie takie problemy są rozwiązywane przez przywołanie małpy piszącej na maszynie ...
piszącej xuq01
5
Lub możesz bezpośrednio wyliczyć warunki rachunku lambda. Znacznie szybciej niż ciągi losowe, ponieważ każde wyjście jest poprawnie sformatowanym terminem. To tak, jakby zastąpić małpy piszące na klawiaturze generatorem gry Szekspira.
Dan D.
11

Jak już wspomniano, jest to tylko wyliczenie terminów z języka bezkontekstowego, więc zdecydowanie wykonalne. Ale kryje się za tym bardziej interesująca matematyka, wchodząca w zakres kombinatoryki anlytycznej.

Artykuł Liczenie i generowanie terminów w binarnym rachunku lambda zawiera sposób rozwiązania problemu zliczania i wiele więcej. Aby uprościć sprawę , używają czegoś, co nazywa się binarnym kalendarzem lambda , który jest po prostu kodowaniem terminów lambda za pomocą wskaźników De Bruijn , więc nie musisz nazywać zmiennych.

Ten artykuł zawiera także konkretny kod Haskella implementujący algorytm ich generowania. To zdecydowanie możliwe.

Zdarzyło mi się napisać implementację ich podejścia w Julii.

phipsgabler
źródło
7

Pewnie. Możemy je bezpośrednio wygenerować zgodnie z definicją terminów lambda.

W Haskell najpierw definiujemy typ danych,

data LC a  =  Var  a                -- Constructor <type> <type> ...
           |  App (LC a) (LC a)     --
           |  Lam  a     (LC a)     --  ... alternatives ...

instance Show a => Show (LC a)      -- `LC a` is in Show if `a` is in Show, and
  where
    show (Var i)    =  [c | c <- show i, c /= '\'']
    show (App m n)  =  "("  ++ show m       ++ " " ++ show n ++ ")"
    show (Lam v b)  =  "(^" ++ show (Var v) ++ "." ++ show b ++ ")"

a następnie za pomocą uczciwego (er) join,

lambda :: [a] -> [LC a]
lambda vars  =  terms 
  where
  terms  =  fjoin [ map Var vars ,
                    fjoin [ [App t s | t <- terms] | s <- terms ] ,
                    fjoin [ [Lam v s | v <- vars ] | s <- terms ] ]

  fjoin :: [[a]] -> [a]
  fjoin xs  =  go [] xs             -- fairer join
      where 
      go [] []  =  []
      go a  b   =  reverse (concatMap (take 1) a) ++ go 
                       (take 1 b ++ [t | (_:t) <- a]) (drop 1 b)

po prostu je wyliczamy, jak np

> take 20 $ lambda "xyz"
[x,y,(x x),z,(y x),(^x.x),(x y),(^y.x),((x x) x),(^x.y),(y y),(^z.x),(x (x x)),
 (^y.y),(z x),(^x.(x x)),((x x) y),(^z.y),(y (x x)),(^y.(x x))]

> take 5 $ drop 960 $ lambda "xyz"
[(((x x) y) (z x)),(^y.(^x.((x x) (x x)))),((^x.(x x)) (^x.(x x))),(^x.((^z.x) 
 y)),((z x) ((x x) y))]

Ω=(λx.xx)(λx.xx)

fjoinjest równoznaczne z Omega monada „s diagonal.

Will Ness
źródło
0

Natknąłem się na jedno narzędzie online, które może generować ciągi przykładowe z wyrażenia regularnego: https://www.browserling.com/tools/text-from-regex . Możesz wygenerować wiele przykładowych wyrażeń lambda, wprowadzając coś takiego:

(\( (lambda \w\. )* \w+ \))* 

Oczywiście, aby uzyskać warunki z dowolnym poziomem zagnieżdżenia, będziesz musiał użyć gramatyki bezkontekstowej, która jest bardziej opisowym narzędziem do definiowania języka niż wyrażenie regularne. Nie natknąłem się na istniejące narzędzie do generowania przykładowych zdań w oparciu o bezkontekstową definicję gramatyki, ale nie ma powodu, dla którego nie można byłoby zbudować.

jaskółka oknówka
źródło
2
λ