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 tu\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 tu: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: ???]