Recently, my advisor (Aaron Stump) and I have been trying to unify induction and coinduction using a single operator and an explicit ordering. I know what you are thinking, awesome! While I could talk for hours about our ideas on how to do this I am instead going to introduce a type theory I think everyone should know of.
While reading over the literature covering duality between induction and coinduction and call-by-name and call-by-value we had the joy of learning about Philip Wadler’s dual calculus (DC) [1,2]. This type theory is the computational view of Gentzen’s classical sequent calculus LK. For more information on LK see . A couple of interesting properties of the dual calculus is that its dual can be embedded in itself. This dual embedding can then be used to show that the call-by-value reduction strategy is dual to the call-by-name reduction strategy. Following on the previous point DC can also be used to show that the call-by-value -calculus is dual to the call-by-name -calculus by first embedding the call-by-value -calculus into DC, taking the dual, and then translating the -calculus back out [1,2]. Cool stuff! In this post I would like to simply define DC and give an intuitive meaning to its judgments. However, there is a twist. The twist is that I have come up with a new syntax for the judgments of DC. While DC is a beautiful theory I am not a fan of DC’s original nor of the version of DC in Kimura’s paper  synatx for judgments. I find them ugly, confusing, and hard to read. I hope the reader will find my syntax a bit more pleasing.
The syntax of DC is defined by the following set of grammars: The first thing the reader who has at least a basic understanding of type theory will notice, is that, there is no function type or -abstraction! It turns out that these can actually be defined! I hope the reader’s head did not just explode. Here are the definitions:
Using these definitions the usual typing rules are now derivable as well as the usual -reduction rule. As for the remaining syntax of DC it is pretty routine. I only comment on a few aspects of it. I call variables input variables and variables output variables or output ports. The output ports will be replaced by the output of (co)terms. Statements can be viewed as commands where is computed with input . The term binds the output port to the return value of the statement . Dually, the coterm binds the input variable in .
DC consists of three judgments. I will first give my new syntax for these judgments, compare my syntax with the original syntax, give an intuitive explanation of the judgments, and finally define them. The syntax is of the three judgments are as follows:
Explanation of the syntax. The arrows in the judgments above indicate the flow of input/output. The first left-pointing arrow indicates that each expression ,, and can assign output to an output port in . Now the right-pointing arrow in the typing judgment indicates that may return a value of type , dually, in the syntax for the cotyping judgment the second left-pointing arrow indicates that takes an input of type . Recall from above that I mentioned that across the propositions-as-types correspondence DC corresponds to Gentzen’s classical sequent calculus LK. LK consists of left and right rules, so additionally the second arrow in the typing and cotyping judgments indicate the type of rules which define the judgments. The rules defining the typing judgment are right rules, hence, the second arrow points right, while the second arrow in the cotyping judgment points left indicating its rules correspond to the left rules of LK.
The syntax used by Kimura was the following:
This syntax is very similar to the original syntax of Wadler, but instead of he used an arrow pointing to which is close to my syntax, but still not as pretty. I find this style syntax to be hard to read, but I do think it makes sense once I understood it. I have this annoying belief that the syntax of a judgment should be sexy enough to make writing out derivations somewhat manageable.
Intuitive meaning of the judgments. Lets first expand the syntax out a bit.
The typing judgment means that when each has a value and is computed then it may either return a value of type or assign a value to one of the output ports of type . Dually, the cotyping judgment means when each has a value then takes an input of type and after computation assigns a value to one of the output ports. Finally, the cut judgments means when each has a value then is computed and assigns a value to one of the output ports. This intuitive explanation behind the judgment helped and continues to help me understand DC. I do not claim authorship of such a great meaning I learned it from . They did a great job explaining the theory.
Definition of the judgments of DC. Finally, I move onto define each judgment. The following is the definition of the typing and cotyping judgment:
Lastly, we have the sole rule of the cut judgment, the cut rule:
A nice feature of this type theory is that it is easy to translate it to a logic equivalent to LK. Lets try this out. We define the following eraser:
Using this eraser we obtain the following logic which is equivalent to LK.
We have the cut rule last:
I might prove this logic equivalent to LK, all truths deducable in this logic are deducible in LK, in a later post. To finish off the definition of DC lets take a look at the reduction rules. I do not pen any specific reduction strategy down here. The reducation rules of DC are:
Well that is the dual calculus. It is a really interesting theory of classical logic. There are quite a few papers on the dual calculus. I sprinkled some throughout the post, but if the reader knows of any I would love to hear about them.