[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