Lambda Calculus Generator

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.

Jasne, to standardowe ćwiczenie kodowania.

Przede wszystkim niech dowolna dwuskładnikowa funkcja obliczeniowa, zwana funkcją parowania. Standardowym wyborem jest$p : \mathbb N^2 \to \mathbb 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 .$k$$n,m$$p(n,m)=k$

Aby wyliczyć terminy lambda, popraw dowolne wyliczenie dla nazw zmiennych: .$x_0,x_1,x_2,\ldots$

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

• jeśli jest parzyste, niech j = i / 2 i zwróci zmienną x $i$$j=i/2$$x_j$
• jeśli jest nieparzyste, niech j = ( i - 1 ) /$i$$j=(i-1)/2$
  • $j$$k=j/2$$n,m$$p(n,m)=k$$N=lambda(n), M=lambda(m)$$(NM)$
  • $j$$k=(j-1)/2$$n,m$$p(n,m)=k$$M=lambda(m)$$(\lambda x_n.\ M)$

$\Lambda$

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 ) ”.

$\mathbb N^2 \simeq \mathbb N$$p$$\mathbb N + \mathbb N \simeq \mathbb N$

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.

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.

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.

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))]

$\Omega = (\lambda x . xx)( \lambda x . xx )$

fjoinjest równoznaczne z Omega monada „s diagonal.

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ć.