2
$\begingroup$

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 (x), 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.

$\endgroup$
  • 1
    $\begingroup$ 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? $\endgroup$ – bill s Sep 8 at 0:03
  • $\begingroup$ @bills I have now clarified the specific requirements. $\endgroup$ – koro Sep 8 at 8:59
  • $\begingroup$ 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. $\endgroup$ – ciao Sep 9 at 3:04
  • $\begingroup$ @ciao Thank you, I'll be sure to look into that. $\endgroup$ – koro Sep 11 at 17:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.