Programming Language and Logic Links

These thread on Lambda the Ultimate has several interesting links to online papers and books about the links between logic and functional programming languages.

What’s interesting is that, with one giant exception (category theory), the mathematics used is among the least fashionable. Most mathematicians can go through their entire careers without learning anything about proof theory and intuitionistic logic, and I think the reason is that both undermine the naive model of mathematical foundations that most mathematicians carry around in their heads. Mathematicians hate thinking about foundations. Whenever a famous open problem turns out to be equivalent to the Continuum Hypothesis, it’s like a family member died, or worse joined a cult.

Proof theory is disconcerting because it treats mathematican proofs as purely syntactic. Mathematicians, whatever their actual philosophy, adopt a working philosophy of Platonism: symplectic manifolds and 7-spheres and von Neumann regular algebras all exist in some nebulous “out there”. While mathematicians occasionally argue that mathematics is just the formal manipulation of symbols, in practice they think of a 7-sphere as an actual object.

In proof theory, mathematics really is just a formal manipulation of symbols. The more elementary parts of proof theory consist of proving one method of representing proof symbolically is the same as another. More advanced proof theory consists of studying topics such as proof normalization, where it is shown that proofs can be systematically rewritten in a particular form. Here are some further links to proof theory texts.

Intuitionistic logic is another field more prominent in computer science than in mathematics. Intuitionistic logic unnerves mathematicians by removing the law of the excluded middle: that a statement is true, or its negation is true. In classical logic, every statement can be (in principle) assigned a value of either true or false. To do the same for intuitionistic logic, some statements must be assigned intermediate truth values (in fact, infinitely many intermediate values become possible). Most mathematicians regard intuitionism as a historical curiosity not particularly of study.

Intuitionism is attractive to computer scientists, because whether or not its axioms correctly model truth, they do model knowability. The law of excluded middle doesn’t apply to knowability. A statement that is not known to be true may also be not known to false. Curry-Howard correspondence between logical formulas and function types has insired study of even weaker logical systems.

Perron-Frobenius on the web

Or, how to make a search engine.

Imagine the web is irreducible, by which I mean you could get from any page to any other by following links; pages without links (and pages no one links to) demonstrate that the web is not irreducible — but this is mathematics, so we are not going to let it worry us. Further, imagine there are millions of monkeyspigeons randomly clicking on links (forming a Markov chain). Perron-Frobenius theory can tell us the probability of these random walks through cyberspace visiting a particular page at an instance in time.

Continue reading

Optimal reduction in the lambda calculus

Lambda the Ultimate links to a new paper, Lambdascope, that describes an implementation of optimal reduction in the lambda calculus.

Optimal, in this case, means the minimum amount of duplication. Usually, when you apply a function in the lambda calculus, you must make a copy of the function body before you start evaluating. In his 1978 thesis, Levy showed that some of this copying could be redundant; in some cases, exponentially so. Levy did not provide an algorithm for optimal reduction, but several have since been invented.

Optimal reduction is a refinement of lazy evaluation. In lazy evaluation, arguments to functions are only copied as needed. Laziness minimizes copying on the right side of function applications, while optimal reduction minimizes it on both sides.

Implementations of optimal reduction are incredibly difficult to understand. The one in the lambdascope paper looks simpler, but I haven’t fully assimilated it.