[TYPES] representation for set of recursive equations?

[Claus Reinke]

> 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?

I'm not sure what recursion or supercombinators have to do with
parameter permutations? If you're worried about partial applications,
you can always eta-expand before permuting, and if you've got a
lambda-calculus that deals with parameter permutations, the ideas
should carry over to sets of recursive equations?

Anyway, once you drop position info as a way to address parameters
locally, you need something else to indicate the correspondence between
formal and actual parameters. One way would be to use labelled multi-sets:
the position doesn't matter, so parameter permutations have equivalent
representations (not syntactically identical, though you could try to order
by labels), and local addressing is via the labels.

Laurent Dami http://cui.unige.ch/~dami/ looked at such things as a basis
for record- and object-calculi and general software composition [1].

Cheers,
Claus

[1]
@article{Dami97a,
  author  = {Laurent Dami},
  title   = {{A Lambda-Calculus with Dynamic Binding}},
  journal = {to appear in Theoretical Computer Science 192(2), special issue on Coordination, Feb
1998},
  year    = 1997,
  sourceURL = {ftp://cui.unige.ch/pub/dami/dynBind.ps.Z},
  abstract = {Dynamic binding denotes a runtime lookup operation which
    extracts values corresponding to some ``names'' from some
    ``environments'' (finite, unordered associations of names and
    values). Many situations related with flexible software assembly
    involve dynamic binding: first-class modules, mobile code,
    object-oriented message passing. This paper proposes a compact
    extension of the lambda-calculus to model dynamic binding, where variables
    are labelled by names, and where arguments are passed to functions
    along named channels.  The resulting formalism preserves familiar
    properties of the lambda-calculus, has a Curry-styletype inference system,
    and has a formal notion of compatibility for reasoning about extensible
    environments. It can encode record and record extensions, as well
    as first-class contexts with context-filling operations, and
    therefore provides a basic framework for expressing awide range of
    name-based coordination mechanisms.  },
  topics  = {FP - Lambda Calculi}
}