[TYPES] representation for set of recursive equations?

jhines at haverford.edu jhines at haverford.edu
Wed Apr 7 23:04:11 EDT 2004


After lambda lifting, a lambda-term looks something like:

F u v = ... u ... v ...
G x y = ... F x y ...

Now, permuting the arguments of a supercombinator both at its definition
and at all of its uses simultaneously does not change anything - the
above is the same as:

F v u = ... u ... v ...
G x y = ... F y x ...

De Bruijn notation is a representation for lambda-terms where, if M is
alpha-equivalent to N, then M and N have identical De Bruijn representations.

Is there a representation for sets of recursive equations where,
analogous to De Bruijn notation, things equivalent by this reordering of
variables have identical representations?

Or, a more reasonable question, where can I read about things similar to this?

Thank you very much!

Johnicholas Hines




More information about the Types-list mailing list