# Lambda calculus reduction in Mathematica

Are there any built-in functions for reducing lambda terms in Mathematica? If not, how might one do it? I've heard of Function, which is good for $$\beta$$-reduction, but it doesn't seem to properly handle $$\alpha$$-conversion. Regarding $$\eta$$-reduction, the best I could find was this snippet from A New Kind of Science (ref): rm[h_, v_] /; FreeQ[h, v] = k[h]

Specifically, what I need is the following:

• A function reduce[term_] which returns term after one step of reduction. It will do one of the following:
• $$\alpha$$-conversion (if necessary) followed by $$\beta$$-reduction
• $$\eta$$-reduction
• Abstraction and application are represented as functions, each taking two arguments:
• Abstraction: $$\lambda x.m$$ is lam[x_, m_]
• Application: $$n\ m$$ is app[n_, m_]
• Other details
• If no reduction is possible, reduce returns term unchanged
• The reduction strategy is normal order
• For $$\alpha$$-conversion, you can choose any method to change the names of variables, such as appending a character (xx´), incrementing a number (x1x2), or changing the name altogether (xa)

Examples of use:

$$\beta$$-reduction

reduce @ app[lam[x, lam[y, x]], a]

lam[y, a]


$$\alpha$$-conversion, $$\beta$$-reduction

reduce @ app[lam[x, lam[y, x]], y]

lam[y´, y]


More complex $$\alpha$$-conversion

reduce @ lam[y´, app[lam[x, lam[y, x]], app[y´, y]]]

lam[y´, lam[y´´, app[y´, y]]]  (* y became y´´ to avoid clashing with the first y´ *)


Normal order

reduce @ lam[x, app[lam[y, y], x]]

lam[y, y]  (* eta-reduction was done before beta-reduction *)


Lambda term in normal form

reduce @ app[a, b]

app[a, b]  (* Nothing can be reduced, so the term is left unchanged *)


If anything is difficult to understand, you're very welcome to ask about it.

• In order to get a good answer, you are going to have to be much clearer about what kinds of functions you are looking for. Can you give examples of what you expect such a function to do? – bill s Sep 8 '19 at 0:03
• @bills I have now clarified the specific requirements. – koro Sep 8 '19 at 8:59
• Find a copy of Gray's "Mastering Mathematica" - IIRC (away from that home so I can't check book), it has an implementation of the LC. – ciao Sep 9 '19 at 3:04
• @ciao Thank you, I'll be sure to look into that. – koro Sep 11 '19 at 17:44