Search code examples
haskellfunctional-programminglambda-calculus

Haskell help : Replacing terms within a lambda-term with new variables! (Simple mistake needs fixing...)


I am trying to write a function, when passed:

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

And a Term, will replace all Terms within the passed Term with a variable from VX respectively.

My function works to a certain extent, for the example:

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

It returns:

S (V1 V1 0) 

Rather than what it should return:

S (V1 V2 0) 

Here is my function along with the tests. Can anyone spot a mistake I have made perhaps?

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)

Solution

  • The issue is that

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

    makes two recursive calls, and intuitively the first one should "consume" any number of variables to generate its output. After that, the second recursive call should not use the variables already "consumed" by the first one.

    In a sense, there is some sort of state which is being modified by each call: the list of variables gets partially consumed.

    To model that, you will need to first write an auxiliary recursive function which returns, together with the new lambda term, the list of not-yet-consumed variables.

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

    Now, when you need to make two recursive calls to aux, you can make the first one, get the list of not-consumed variables from its result, and make the second recursive call using that list.

    (A more advanced solution would be to use a State [Var] monad, but I guess you want to write a basic solution.)