sequoia

Sequoia is an implementation of classical logic in a sequent calculus, embedded in intuitionistic logic. It is implemented as a Haskell EDSL, and is fairly full-featured, if sparsely documented (at best).

Sequoia is experimental; do not use it to pilot spacecraft, unless you really, really want to.

Sequent calculus

A sequent states that, together, all the things to the left of the symbol (called turnstile, pronounced proves) suffice to prove at least one of the things on the right:

all of these prove some of these

The elements of are treated conjunctively (hence all), while the elements of are treated disjunctively. Computationally, we interpret as a kind of function, as a kind of sequence, and as a kind of choice, and thus we can think of as inputs and as outputs.

Sequents are rarely seen alone, however, and instead are grouped with premises written above a line (the line of inference) to make rules, like this rule Ill name dull:

dull\

Typically we read these bottom-up; this says to infer that proves , we must prove that proves . (This is true, though not particularly helpful.)

Axioms are rules which can be employed without any further premises. For example the init rule states that an input in can become an output in :

init A, , A

Rules take premises to conclusions (the sequent underneath the line), and thus the line of inference can be understood as another kind of function arrow, mapping zero or more premise sequents to a conclusion sequent. And since sequents are themselves a kind of function, mapping hypotheses to consequents, we can see that sequent calculus proofs correspond with higher-order functional programs.

For that reason, sequoia can map rules like init straightforwardly onto functions like id, and the implementation further takes full advantage of the relationship beween the sequent calculus and continuation-passing style to provide a full suite of polarized connectives (datatypes corresponding to logical operators), including positive and negative falsities, truths, disjunctions, conjunctions, implications, quantifiers, etc.

Furthermore, sequoia offers introduction and elimination rules for aach connective, grouped together into a typeclass. (This is done to allow for different sets of rules, even for the same connectives, to be used for e.g. linear logics, altho I havent implemented this yet.) The built-in type Seq in Sequoia.Sequent implements all of them. Inverses are also available where provable, as are many algebraic properties for the connectives.

It is possible to perform effects, but this hasnt been explored much yet. However, youve got the full power of call/CC available, not to mention delimited continuations (Sequoia.Calculus.Control), and while it isnt particularly convenient at the moment, theres even a monad transformer to lift actions into sequents.