dual calculus

The notation makes use of a pair of mnemonic conventions:

• unary term formers are written postfix, while unary coterm formers are written prefix;
• angle brackets enclose terms, square brackets enclose coterms, and parentheses enclose statements.

Here is some intuition for these constructs.

• forms a pair of two terms and .
• takes a continuation and essentially precomposes the first projection with it. In other words, turns from a continuation that expects a value of type into a continuation that expects a value of type . is similar.
• injects the term into a sum on the left; injects the term into a sum on the right.
• performs case analysis on a sum value, executing in case it is a left value and in case it is a right value.
• converts a coterm into a value. Specifically, a coterm that expects a value of type becomes a continuation of type .
• converts a term into a covalue. Specifically, a term becomes a covalue that, upon receiving a continuation value , passes the result of evaluating to .
• abstracts over the covariable , converting the statement into a term that yields whatever value is passed to . Likewise abstracts over the variable , converting the statement into a coterm that awaits a value for .
• Function abstraction has the usual interpretation. Function application works a little differently, though.

There are three kinds of type judgments: one for terms, one for coterms, and one for commands.

All judgments involve two lists of assumptions, one on each side of a turnstile , just as in the sequent calculus. On the left, means that the variable stands for a value of type . On the right, means that the covariable stands for a covalue of type (i.e., a computational context with a hole of type ).

For terms, means that, given the assumptions in and , the term has type . Computationally, it means that, if each variable in is assigned a value of appropriate type, then will either evaluate to a value of type or pass to a covariable in a value of appropriate type.

For coterms, means that, given the assumptions in and , the coterm has type . Computationally, it means that, if each variable in is assigned a value of appropriate type and is passed a value of type , then it will pass to some covariable in a value of appropriate type.

It may seem odd that judgments are written on the right for terms and on the left for coterms. However, they correspond respectively to right and left rules in the sequent calculus, so the choice makes sense. Also observe that the computational interpretation has a disjunctive flavor for term judgments and a conjunctive flavor for coterm judgments.

Finally, for statements, means that, given the assumptions in and , the statement is well-typed. Computationally, it means that, if each variable in is assigned a value of appropriate type, then will pass to some covariable in a value of appropriate type.

Can we recover elimination rules from the left rules?

Yes, we can. Every left rule is very much like the contrapositive of an elimination rule. An elimination rule for says something like “give me a value of type and I will extract some data from it.” A left rule for says something like “give me a place to put some data from a value of type and I will give you a place to put a value of type .” To recover an elimination rule, we simply need to feed in a value of type and tell the left rule to put the data right here. That is, if , we write , where is an expression that applies a left rule, using as the final continuation.