Haskell справка: Замена терминов в лямбда-члене новыми переменными! (Простая ошибка требует исправления ...)

Question

Я пытаюсь написать функцию, когда передается:

variables VX = ["v1",..."vn"]

И Term заменяет все Terms в переданном Term на variable from VX соответственно.

Моя функция работает в определенной степени, например:

S ((\a. \x. (\y. a c) x b) (\f. \x. x) 0)

Она возвращает:

S (V1 V1 0) 

Вместо того, что она должна вернуть:

S (V1 V2 0) 

Вот моя функция вместе с тестами. Может ли кто-нибудь заметить мою ошибку?

termToExpression :: [Var] -> Term -> Expression
termToExpression [] a = termToExpr a
termToExpression _ (TermVar y) = ExpressionVar y
termToExpression (x : _) (TermLambda a b) = ExpressionVar x 
termToExpression (x : xs) (TermApp n m) = ExpressionApp (termToExpression (x : xs) n) (termToExpression (x : xs) m)

Answer 1

Проблема в том, что

ExpressionApp (termToExpression (x : xs) n) (termToExpression (x : xs) m)

делает два рекурсивных вызова, и интуитивно первый из них должен «потреблять» любое количество переменных для генерации своего вывода. После этого второй рекурсивный вызов не должен использовать переменные, уже "использованные" первым.

В некотором смысле существует какое-то состояние, которое изменяется при каждом вызове: список переменных получает частично потреблены.

Чтобы смоделировать это, вам нужно сначала написать вспомогательную рекурсивную функцию, которая возвращает вместе с новым лямбда-термином список еще не использованных переменных.

aux :: [Var] -> Term -> (Expression, [Var])

Теперь, когда вам нужно сделать два рекурсивных вызова aux, вы можете сделать первый, получить список неиспользованных переменных из его результата и сделать второй рекурсивный вызов, используя этот список.

(Более продвинутое решение - использовать монаду State [Var], но я думаю, вы хотите написать базовое решение c.)