Да, я выкладываю другой ответ. И это все еще может быть не совсем то, что вы ищете. Но я думаю, что это может быть полезным, тем не менее. Это на Хаскеле.
data LExpr = Lambda Char LExpr
| Atom Char
| App LExpr LExpr
instance Show LExpr where
show (Atom c) = [c]
show (App l r) = "(" ++ show l ++ " " ++ show r ++ ")"
show (Lambda c expr) = "(λ" ++ [c] ++ ". " ++ show expr ++ ")"
Итак, здесь я подготовил базовый алгебраический тип данных для выражения лямбда-исчисления. Я добавил простой, но эффективный пользовательский экземпляр Show.
ghci> App (Lambda 'a' (Atom 'a')) (Atom 'b')
((λa. a) b)
Ради интереса я добавил простой reduce
метод с помощником replace
. Предупреждение: не тщательно продумано или проверено. Не использовать в промышленных целях. Не может обрабатывать некоторые неприятные выражения. : P
reduce (App (Lambda c target) expr) = reduce $ replace c (reduce expr) target
reduce v = v
replace c expr av@(Atom v)
| v == c = expr
| otherwise = av
replace c expr ap@(App l r)
= App (replace c expr l) (replace c expr r)
replace c expr lv@(Lambda v e)
| v == c = lv
| otherwise = (Lambda v (replace c expr e))
Кажется, это работает, хотя на самом деле меня отвлекают. (it
в ghci относится к последнему значению, оцененному в приглашении)
ghci> reduce it
b
Так что теперь самое интересное, rotate
. Поэтому я решил, что могу просто снять первый слой, и, если это лямбда, отлично, я сохраню идентификатор и продолжу детализацию до тех пор, пока не достигну не-лямбды. Тогда я просто вставлю лямбду и идентификатор обратно в «последнее» место. Если это не была лямбда, то ничего не делай.
rotate (Lambda c e) = drill e
where drill (Lambda c' e') = Lambda c' (drill e') -- keep drilling
drill e' = Lambda c e' -- hit a non-Lambda, put c back
rotate e = e
Простите неимагнитивные имена переменных. Отправка этого через ghci показывает хорошие признаки:
ghci> Lambda 'a' (Atom 'a')
(λa. a)
ghci> rotate it
(λa. a)
ghci> Lambda 'a' (Lambda 'b' (App (Atom 'a') (Atom 'b')))
(λa. (λb. (a b)))
ghci> rotate it
(λb. (λa. (a b)))
ghci> Lambda 'a' (Lambda 'b' (Lambda 'c' (App (App (Atom 'a') (Atom 'b')) (Atom 'c'))))
(λa. (λb. (λc. ((a b) c))))
ghci> rotate it
(λb. (λc. (λa. ((a b) c))))