Symmetric λ-calculus is a generalization of λ-calculus to make contexts and terms more on par with each other, though it follows that one needs to leave terms alone (almost) and introduce ntexts instead (called “out contexts” vs. “in contexts” below). You should definitely blame User:arseniiv for making this essential thing in March, 2020. Here, a simply typed variant is given.
Parts marked as NB are notes to myself.
In and out contexts .
Only well-typed terms are considered, for which a typing is proven. Typing rules are the following:
- whether and .
- whether and . [NB: I need to check if can have more general types or, conversely, even these two aren’t correct (vs. the case when .]
- whether .
- whether .
There is a reduction akin to β-reduction from the usual calculus, . Informally, is a plumbing of all free in to all free in . I’ll define this function formally a bit later. [NB: do it!]
Note as we presuppose well-typed, we should have and .
I think this system is equivalent to λ-calculus if one restricts term formation in the following way: is a half-restricted term iff, inductively, each is a half-restricted term or is of form ; and a half-restricted term is restricted iff it does have no two different subterms for any . A restricted term represents a mapping from out-variables to in-variables, i. e. each output gets a value from a single input. Now, only restricted terms are allowed (of those), and we should also forbid to abstract on an out-variable not occurring in a term ( is invalid if is not free in ).
How should one treat the unrestricted terms is up to the future. There are at least three possibilities: many simultaneous outputs and many alternative outputs, with choice being on a caller or a callee.
To be continued maybe.
Compared to the usual calculus
With the current choice of syntax, the old abstraction corresponds to the backwards one . All terms now have variables representing their value(s). For example, old is mapped to , old is mapped to (there should be no need to distinguish the order in which complementary abstractions are added) [NB: make sure].
I added to be able to represent something like , but now I can’t make anything out of it. Maybe I should rethink the way application is defined. [NB: ???]