2013-11-23
Programming Language Theory Notation

I love to program in various languages, and I like to study (and often, comment upon) the various features (or lack) in these programming languages. I’m also very interested in Programming Language Metatheory, which I will informally define as the relationship between a programming language’s syntax, semantics, and purpose. This includes proof systems about program correctness. My formal training as a Computer Scientist was fun because I was able to learn an entirely different level of programming and an associated notation: the language of formal proofs.

One of the important characteristics I need from my blogging and authoring technology is the ability to express proofs, semantics and the notation necessary for theoretical computer science.

Definition of Programming Language

  • A notation for giving instructions
  • A notation for describing inductive structures
  • A type system

Examples of Programs

A Java program
public class HelloWorld
{
   public static void main(String[] args)
   {
      System.out.println("Hello, World");
   }
}
Driving Directions
1.  2 blocks North
2.  Left at Wilson Rd
3.  East for 3 blocks.
Mathematical Transformation

The solutions of $$ax^2 + by + c = 0$$ are given by \eqref{eq:quad} below:

\begin{align} x = \frac{ - b \pm \sqrt {b^2 - 4ac} }{2a} \label{eq:quad} \end{align}
A Logical Proof

Hmmm. So the wonderful bussproofs.sty that is used for doing Prawitz and Gentzen style proof trees is not available in my MathJax-enabled LaTex compatibility mode. This sucks, but also presents a wonderful opportunity in terms of implementing a better, more interactive proof display structure. I’m thinking AngularJS would be a great way to create directives that could contain expressions in LaTeX, but that would wield the layout engine of HTML5.

Meanwhile, I have some fragmentary attempts in displaying proofs below…

Let’s try a simple Gentzen Sequent, but without any tree notation:

$$ \def \fCenter{\vdash} $$

$$ B,\Gamma \fCenter A $$

$$ \Gamma \fCenter B\backslash A $$

Cool, that sort of worked. Now let’s try a sequent deduction. Here, the deduction in the Lambek calculus that from $$A/B$$ and $$B$$ we can conclude $$A$$ in the shared context $$\Gamma,\Delta$$.

\begin{aligned} \Gamma \fCenter A/B & & & & \Delta \fCenter B \\\\ \hline & & \Gamma,\Delta \fCenter A \end{aligned}

The above deduction isn’t bad, and not too hard. But I didn’t get to annotate my line with a rule. Let’s try the next Lambek rule, where I’ll try to label the line.

\begin{aligned} \Gamma \fCenter B & & & & \Delta \fCenter B\backslash A \\\\ \hline & & & & {\scriptsize[\backslash E]} \\\\ & & \Gamma,\Delta \fCenter A \end{aligned}

Ugh. That doesn’t look right. The rule annotation $$[\backslash E]$$ is showing up on its own line and I cannot get it to play nicely with the \hline.

I guess I can use two \hline and place the rule annotation between them:

\begin{aligned} \Gamma \fCenter B & & & & \Delta \fCenter B\backslash A \\\\ \hdashline & & & & & & {\scriptsize[\backslash E]} \\\\ \hline & & \Gamma,\Delta \fCenter A \end{aligned}

So here I’ll try to use the \cfrac (continued fraction) capability:

$$ \cfrac {\Gamma \fCenter B \hspace{5ex} \Delta \fCenter B\backslash A} {\Gamma,\Delta \fCenter A} {\hspace{2ex}\scriptsize[\backslash E]} $$

Works nicely and places the rule annotation. Let’s see if it holds up with larger proofs (this is an incomplete proof of an obvious theorem; I have left out the variable introduction parts.)

$$ \cfrac {\Gamma \fCenter B \hspace{5ex} \cfrac {B \Delta \fCenter A} {\Delta \fCenter B \backslash A} {\hspace{2ex}\scriptsize[\backslash I]}} {\Gamma,\Delta \fCenter A} {\hspace{2ex}\scriptsize[\backslash E]} $$

Other examples of Program

  • Circuit Diagram

  • Rube Goldberg Machine

  • Musical Score

  • Cooking Recipe