Symmetric λ-calculus

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.
== Syntax ==
Variables x, y.
Types T, U ::= \alpha, \beta, \ldots \mid \bullet \mid T \succ U \mid T \to U.
In and out contexts \Gamma, \Delta ::= \varepsilon \mid \Gamma, x : T.
Terms t, u ::= x \mid t + u \mid t u \mid x.t \mid t\,{.}x.
Only well-typed terms t are considered, for which a typing \Gamma \vdash t : T \dashv \Delta is proven. Typing rules are the following:
* \Gamma, x : T \vdash x : T \succ \bullet \dashv \Delta.
* \Gamma \vdash y : \bullet \to U \dashv \Delta, y : U.
* \Gamma \vdash t + u : T \dashv \Delta whether \Gamma \vdash t : T \dashv \Delta and \Gamma \vdash u : T \dashv \Delta.
* \Gamma \vdash t u : U \dashv \Delta whether \Gamma \vdash t : T \succ U \dashv \Delta and \Gamma \vdash u : U \to T \dashv \Delta. [NB: I need to check if t, u can have more general types or, conversely, even these two aren’t correct (vs. the case when T = \bullet.]
* \Gamma \vdash t\,{.}x : T \succ U \dashv \Delta whether \Gamma, x : T \vdash t : U \dashv \Delta.
* \Gamma \vdash y.t : U \to T \dashv \Delta whether \Gamma \vdash t : T \dashv \Delta, y : U.
== Semantics ==
There is a reduction akin to β-reduction from the usual calculus, (t\,{.}x)(y.u) \to_\beta [t, x; y, u]. Informally, [t, x; y, u] is a plumbing of all free x in t to all free y in u. I’ll define this function formally a bit later. [NB: do it!]
Note as we presuppose (t\,{.}x)(y.u) well-typed, we should have \Gamma, x : T \vdash t : U \dashv \Delta and \Gamma \vdash u : U \dashv \Delta, y : T.
I think this system is equivalent to λ-calculus if one restricts term formation in the following way: t + u is a half-restricted term iff, inductively, t, u each is a half-restricted term or is of form xy; and a half-restricted term is restricted iff it does have no two different xy, x'y subterms for any y. 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 t + u terms are allowed (of those), and we should also forbid to abstract on an out-variable not occurring in a term (y.t is invalid if y is not free in t).
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 \lambda x.t corresponds to the backwards one t\,{.}x. All terms now have variables representing their value(s). For example, old x is mapped to xy, old \lambda x.x is mapped to y.xy\,{.}x (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 \lambda x.(fx)x, but now I can’t make anything out of it. Maybe I should rethink the way application is defined. [NB: ???]
Category:2020
Category:Computational models