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 returnstermafter 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_]
- Abstraction: $\lambda x.m$ is
- Other details
- If no reduction is possible,
reducereturnstermunchanged - 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 (
x→x´), incrementing a number (x1→x2), or changing the name altogether (x→a)
- If no reduction is possible,
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.
