Wyzwanie polega na napisaniu interpretera dla niepisanego rachunku lambda w jak najmniejszej liczbie znaków. Nietypowy rachunek lambda definiujemy w następujący sposób:
Składnia
Istnieją następujące trzy rodzaje wyrażeń:
Wyrażenie lambda ma postać, w
(λ x. e)
którejx
może być dowolną nazwą zmiennej prawnej ie
dowolnym wyrażeniem prawnym. Tutajx
jest nazywany parametrem ie
nazywa ciało funkcji.Dla uproszczenia dodajemy dodatkowe ograniczenie, że nie może istnieć zmienna o takiej samej nazwie jak
x
obecnie w zakresie. A zaczyna być zmienne w zakresie, gdy pojawi się nazwa pomiędzy(λ
a.
i zatrzymuje się w zakresie w odpowiedni)
.- Aplikacja funkcji ma formę,
(f a)
gdzief
ia
są wyrażeniami prawnymi. Tutajf
nazywa się funkcję ia
nazywa się argumentem. - Zmienna ma postać
x
gdziex
jest legalną nazwą zmiennej.
Semantyka
Funkcja jest stosowana przez zastąpienie każdego wystąpienia parametru w treści funkcji argumentem. Bardziej formalnie ekspresja formy ((λ x. e) a)
, w której x
jest nazwą zmienne, e
i a
są wyrażeniami, ocenia się (lub zmniejsza) do ekspresji e'
, gdzie e'
jest wynikiem zastąpienia w każdym wystąpieniu x
w e
z a
.
Forma normalna jest wyrażeniem, którego nie można dalej oceniać.
Wyzwanie
Twoim zadaniem, jeśli zdecydujesz się to zaakceptować, jest napisanie interpretera, który jako dane wejściowe przyjmuje wyrażenie niepisanego rachunku lambda niezawierającego wolnych zmiennych i generuje jako wynik normalną formę wyrażenia (lub wyrażenie alfa zgodne z nim) . Jeśli wyrażenie nie ma normalnej postaci lub nie jest prawidłowym wyrażeniem, zachowanie jest niezdefiniowane.
Rozwiązanie o najmniejszej liczbie znaków wygrywa.
Kilka uwag:
- Dane wejściowe można odczytać ze standardowego wejścia lub z nazwy pliku podanej jako argument wiersza poleceń (wystarczy zaimplementować jedno lub drugie - nie oba). Wyjście przechodzi na standardowe wyjście.
- Alternatywnie możesz zdefiniować funkcję, która pobiera dane wejściowe jako ciąg znaków i zwraca dane wyjściowe jako ciąg znaków.
- Jeśli występują problemy ze znakami spoza ASCII, możesz użyć znaku odwrotnego ukośnika (
\
) zamiast λ. - Liczymy liczbę znaków, a nie bajtów, więc nawet jeśli plik źródłowy jest zakodowany jako Unicode λ, liczy się jako jeden znak.
- Prawne nazwy zmiennych składają się z jednej lub większej liczby małych liter, tj. Znaków od a do z (nie trzeba obsługiwać nazw alfanumerycznych, wielkich liter lub liter spoza alfabetu łacińskiego - chociaż takie postępowanie oczywiście nie unieważnia rozwiązania).
- Jeśli chodzi o to wyzwanie, nawiasy nie są opcjonalne. Każde wyrażenie lambda i każda aplikacja funkcji będzie otoczona dokładnie jedną parą nawiasów. Żadna nazwa zmiennej nie będzie otoczona nawiasami.
- Cukier syntaktyczny, taki jak pisanie
(λ x y. e)
dla(λ x. (λ y. e))
, nie musi być obsługiwany. - Jeśli do oceny funkcji wymagana jest głębokość rekurencji większa niż 100, zachowanie jest niezdefiniowane. To powinno być wystarczająco niskie, aby można je było wdrożyć bez optymalizacji we wszystkich językach, a jednocześnie wystarczająco duże, aby móc wykonywać większość wyrażeń.
- Możesz także założyć, że odstępy będą takie jak w przykładach, tj. Bez spacji na początku i na końcu danych wejściowych lub przed a
λ
lub.
dokładnie jedną spacją po a.
oraz między funkcją i jej argumentem a po aλ
.
Przykładowe wejście i wyjście
Wejście:
((λ x. x) (λ y. (λ z. z)))
Wynik:
(λ y. (λ z. z))
Wejście:
(λ x. ((λ y. y) x))
Wynik:
(λ x. x)
Wejście:
((λ x. (λ y. x)) (λ a. a))
Wynik:
(λ y. (λ a. a))
Wejście:
(((λ x. (λ y. x)) (λ a. a)) (λ b. b))
Wynik:
(λ a. a)
Wejście:
((λ x. (λ y. y)) (λ a. a))
Wynik:
(λ y. y)
Wejście:
(((λ x. (λ y. y)) (λ a. a)) (λ b. b))
Wynik:
(λ b. b)
Wejście:
((λx. (x x)) (λx. (x x)))
Dane wyjściowe: cokolwiek (jest to przykład wyrażenia, które nie ma normalnej postaci)
Wejście:
(((λ x. (λ y. x)) (λ a. a)) ((λx. (x x)) (λx. (x x))))
Dane wyjściowe:
(λ a. a)
(Jest to przykład wyrażenia, które nie normalizuje się, jeśli oceniasz argumenty przed wywołaniem funkcji, i niestety przykład, dla którego moje próbowane rozwiązanie kończy się niepowodzeniem)Wejście:
((λ a. (λ b. (a (a (a b))))) (λ c. (λ d. (c (c d)))))
Dane wyjściowe:
`(λ a. (λ b. (a (a (a (a (a (a (a (a b))))))))))
oblicza 2 ^ 3 w liczbach kościelnych.
(\y. a)
.