We recently had an internal presentation covering a variety of fundamental theories of computation that underly several important programming languages. Here are a few papers that might help explain those theories in more depth (if not the actual interpreters we developed):
In team software projects, significant problems are often caused by inconsistent assumptions between two or more people. We often resort to informal agreements on paper (or in email) that may or may not remain consistent with our code over time. But these specifications don’t need to be informal in the right programming environments, because types are propositions, and proofs are programs.
To what extent can this observation save us from ourselves?
I’ve been working in KDB fairly frequently on my current project. Today, I had some time on my lunch break to figure out how to use it to write a basic prefix interpreter. I wanted to keep it to one anonymous expression, which meant that I couldn’t use explicit recursion. I also wanted to make it as compact as possible. Here’s the result:
{{x[{(y[x;y])[z]}[x;y]]}[x;{x[{(y[x;y])[z]}[x;y]]}]}[{$[y~();();$[-11h=type y;({{x[{(y[x;y])[z]}[x;y]]}[x;{x[{(y[x;y])[z]}[x;y]]}]}[{$[z~();(exit[0];-1 string y);$[y in key z 0;(z 0) y;(x[y])[z 1]]]}][y])[z];$[0<>type y;y;.[x[y[0]][z];{(x[z])[y]}[x;z] each 1 _ y]]]]}]
The Earley Parser is a general method for parsing any context-free grammar. Although it avoids the significant faults of its narrower associates (e.g.: infinite loops on left recursive rules in top-down parsers, or reduce-reduce conflicts on ambiguous rules in table-based parsers), it’s a very inefficient algorithm.
A few years back I implemented Earley’s algorithm, and bound it to a small Scheme interpreter I’d made. The result is a simple environment for interactively creating parsers and experimenting with their output:
An example of an interaction one might have:
> (define arith-parser
(make-parser
(concat
“E ::= Val | Val Op E;”
“Val ::= Num | \”(\” E \”)\”;”
“Op ::= \”+\” | \”-\” | \”*\” | \”/\”;”
“Num ::= ‘[0-9]+’;”
)))> (arith-parser “(5+3)*2″)
(E (VAL “(” (E (VAL (NUM “5″)) (OP “+”) (E (VAL (NUM “3″)))) “)”) (OP “*”) (E (VAL (NUM “2″))))
A year or so ago, I wrote this small interactive interpreter as a tool to help with some other work I was doing. It might be of some general interest to anybody interested in Scheme.
QuickCheck is a clever tool for testing whether software works correctly under a set of rules constraining its behavior (ie: its specification). The rules that the system accepts (written as Erlang programs) generate programs to evaluate or – as in a recent case study – messages to send to remote servers. After a fault is detected, the QuickCheck system will simplify the generated case as much as possible.
From this paper via lambda-the-ultimate.
