First-order logic a la carte

What’s covered in today’s post isn’t strictly a trick for handling binding (in this case, binding is handled by HOAS, though the method doesn’t appear to be limited to using HOAS).  However, the approach that’s summaried, datatypes a la carte, is a neat trick that I’ve only recently come across.  In short, the trick can be boiled down to: “build larger datatypes from smaller datatypes by taking their coproduct”.

The following article demonstrates one benefit of doing this: building a datatype representing first-order formulae, we can then define a series of transformation steps (at each stage eliminating a logical connective) which transforms an arbitrary FOL formula into implicative normal form.  What’s really unique about this approach is that every step of the transformation is guaranteed, by the type system, to eliminate the corresponding connective from the input formula.

By Kenneth Knowles, in the Monad.Reader Issue 11, available from the Monad.Reader archive:

Classical first-order logic has the pleasant property that a formula can be reduced to an elegant implicative normal form through a series of syntactic simplifications. Using these transformations as a vehicle, this article demonstrates how to use Haskell’s type system, specifically a variation on Swierstra’s “Data Types a la Carte” method, to enforce the structural correctness property that these constructors are, in fact, eliminated by each stage of the transformation.

1 Response to “First-order logic a la carte”


  1. 1 Satellite TV May 10, 2014 at 1:01 pm

    What’s up to every one, the contents present at this website are actually
    amazing for people knowledge, well, keep up the nice work fellows.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: