Lambda the Ultimate

A Lambda Calculus for Real Analysis

Abstract Stone Duality is a revolutionary paradigm for general topology that describes computable continuous functions directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.

This language is applied to the Intermediate Value Theorem: the solution of equations for continuous functions on the real line. As is well known from both numerical and constructive considerations, the equation cannot be solved if the function "hovers" near 0, whilst tangential solutions will never be found.

In ASD, both of these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of overtness. The zeroes are captured, not as a set, but by higher-type modal operators. Unlike the Brouwer degree, these are defined and (Scott) continuous across singularities of a parametric equation.

Expressing topology in terms of continuous functions rather than sets of points leads to treatments of open and closed concepts that are very closely lattice- (or de Morgan-) dual, without the double negations that are found in intuitionistic approaches. In this, the dual of compactness is overtness. Whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD.

Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory.

Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated Jean-Yves Girard's regrettably out-of-print Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX.

Certified Programming With Dependent Types

From the introduction:

We would all like to have programs check that our programs are correct. Due in no small part to some bold but unfulfilled promises in the history of computer science, today most people who write software, practitioners and academics alike, assume that the costs of formal program verification outweigh the benefits. The purpose of this book is to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science. Beyond the convincing, I also want to provide a handbook on practical engineering of certified programs with the Coq proof assistant.

This is the best Coq tutorial that I know of, partially for being comprehensive, and partially for taking a very different tack than most with Adam's emphasis on proof automation using Coq's Ltac tactic language. It provides an invaluable education toward understanding what's going on either in LambdaTamer or Ynot, both of which are important projects in their own rights.

Please note that Adam is explicitly requesting feedback on this work.

ActorScript(TM): Industrial strength integration of local and nonlocal concurrency for Client-cloud Computing by Carl Hewitt, 2009.

ActorScript is based on a mathematical model of computation that treats “Actors” as the universal primitives of concurrent digital computation [Hewitt, Bishop, and Steiger 1973; Hewitt 1977]. Actors been used both as a framework for a theoretical understanding of concurrency, and as the theoretical basis for several practical implementations of concurrent systems.

I hope I do not need to introduce Carl Hewitt or his Actor model. This paper is a modern attempt to expose that model via a practical PL.

I recently came across the language SequenceL, which it seems NASA is using in some of its human spaceflight programs. SequenceL is described as a high-level language for declarative computation on nonscalars. One of the key features of the language appears to be the avoidance of the need to explicitly specify recursive or iterative operations. For example, given the function definition

Search(scalar Target, tuple [Subscript, Word]) = 
    Subscript when Word = Target 

which applies to tuples, the programmer can apply the function directly to lists of tuples without any need to specify how that application will be performed, e.g.

search(fox,[[1,dog],[2,cat],[3,fox],[4,parrot]]) → 3 
search(rabbit,[[1,dog],[2,cat],[3,fox],[4,parrot]]) → [] 

The language designers (Daniel Cooke and J. Nelson Rushton) claim that this kind of thing leads to more concise and readable code, and a more direct representation of a specification.

Unfortunately, the SequenceL website appears to be inaccessible at the moment. However, Daniel Cooke's site includes links to a number of papers and talks that describe SequenceL. In particular, the paper Normalize, Transpose, and Distribute: An Automatic Approach for Handling Nonscalars provides a detailed description of the "Consume-Simplify-Produce/Normalize-Transpose" approach that is embodied by SequenceL. There's also an overview of SequenceL available through CiteSeer.

Verified Programming in Guru is a tutorial introduction to Guru:

GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs.

In comparison to Coq:

GURU is inspired largely by the COQ theorem prover, used for formalized mathematics and theoretical computer science, as well as program verification. Like COQ, GURU has syntax for both proofs and programs, and supports dependent types. GURU does not have as complex forms of polymorphism and dependent types as COQ does. But GURU supports some features that are difficult or impossible for COQ to support, which are useful for practical program verification. In COQ, the compiler must be able to confirm that all programs are uniformly terminating: they must terminate on all possible inputs. We know from basic recursion theory or theoretical computer science that this means there are some programs which really do terminate on all inputs that the compiler will not be able to confirm do so. Furthermore, some programs, like web servers or operating systems, are not intended to terminate. So that is a significant limitation. Other features GURU has that COQ lacks include support for functional modeling of non-functional constructs like destructive updates of data structures and arrays; and better support for proving properties of dependently typed functions.

The tutorial is worth a read to anybody new to this style of programming as it is one of the most gentle introductions to dependent types and automated program verification that I've seen.

In a Qilang mailing list email Marker Tarver, creator of Qi, says

In a month I will be packing to go to India; this time for an extended
period. But its also a goodbye to Qi and computing. At some point
you have to acknowledge that Qi doesn't pay its way. It was fun
though and I'm not sad about it.

Qi has been a journey that began nearly 20 years ago when I was a very
different person and worked for a university. But the book on Qi II
marks a natural watershed. I need to move on. By September I will be
gone.

The list of accepted papers is out for the IFIP Working Conference on Domain Specific Languages. Happily for me, the program reveals much interest in languages for reasoning, decision making, and search. Even among people who are not my coauthors. :)

Declarative programming tends to attract skepticism because it has the reputation of poor and hard-to-control performance. The approach of DSL embedding appears to ameliorate this problem, and the success of SAT solvers appears to chip away at this reputation.

Meanwhile, the call for papers is out for Principles and Practice of Declarative Programming 2009, which has a venerable program committee. The submission deadline is May 7.

Qi II has been released. Qi is a functional programming language built on top of Common Lisp. It has an optional static type system based on sequent calculus and a general focus on logic based programming. For version II, see the what's new page. Rule closures in particular look very interesting.

Unlike Qi I, Qi II allows you to embed sequent rules within functions, evaluating them to closures. These rule closures are type checked and are permeable to having their variables lexically bound from outside the scope of the rule itself. These devices enable the student of computational logic to effortlessly code complex logical systems of all descriptions. Thus the rule

let PTerm/X (replace-by X Term P)
PTerm/X, (all X P) >> Q;
____________________
(all X P) >> Q;

allows universally quantified assumptions to be instantiated to new premises. This rule can be embedded into a Qi II function called all-left which does precisely this job. The rule is turned into a closure by the rule function which is then applied to the problem (list of sequents).

(define all-left
{term --> [sequent] --> [sequent]}
Term S -> ((rule let PTerm/X (replace-by X Term P)
PTerm/X, (all X P) >> Q;
____________________
(all X P) >> Q;) S))

FPQi devotes a hundred pages to the exploration of this powerful construction.

Also with this release is a new book: Funcitonal Programming in Qi.

Earlier versions of Qi have been mentioned on LtU here and here.

Anand S. Rao (1996). AgentSpeak(L): BDI Agents speak out in a logical computable language.

Rao's AgentSpeak(L) is a Prolog-like resolution-based language, but which is extended to support agent-based programming in several ways, most importantly:

1. It extends the language, so that clauses can talk about not just satisfaction of predicates, but also of an agent desiring to bring about a predicate, and desiring to find out whether a predicate is true; and to distinguish between normal goals and special goals relevant to the BDI model (Belief-Desire-Intention model);
2. It amends the resolution engine to support what Rao calls reactive concurrency, where agents form plans via a process resembling SLD-resolution, but plans are formed or abandoned on the basis of agent-internal reactions called triggering events.

Rao and Georgeff's work on BDI agents and procedural reasoning together constitutes one of the most important contributions to the theory of agents in AI, a topic which hasn't been discussed much here on LtU, but was raised in the Agent Oriented Programming story.

Linear Logical Algorithms, Robert J. Simmons and Frank Pfenning, 2008.

Bottom-up logic programming can be used to declaratively specify many algorithms in a succinct and natural way, and McAllester and Ganzinger have shown that it is possible to define a cost semantics that enables reasoning about the running time of algorithms written as inference rules. Previous work with the programming language Lollimon demonstrates the expressive power of logic programming with linear logic in describing algorithms that have imperative elements or that must repeatedly make mutually exclusive choices. In this paper, we identify a bottom-up logic programming language based on linear logic that is amenable to efficient execution and describe a novel cost semantics that can be used for complexity analysis of algorithms expressed in linear logic.

In my last post, I linked to a paper by Ganzinger and McAllester about specifying algorithms as logic programs, and a) admired how concise and natural the programs were, and b) was sad that the logic programs used some "non-logical" operations, such as deletion.

So, what does it mean for an operation to be "non-logical", and why is it a bad thing? Roughly speaking, you can think of the analogy: non-logical operations are to logic programs what impure operations are to functional programs -- they are features which break some parts of the equational theory of the language. Now, the Curry-Howard correspondence for functional programs says that types are propositions, and programs are proofs. It turns out that a different version of this correspondence holds for logic programs: in logic programming, a set of propositions is a program, and the execution of a program corresponds to a process of proof search -- you get a success when execution finds a proof of the goal.

When you have nonlogical operations in your logic programming language, you've introduced operators that don't correspond to valid rules of inference, so even if your logic program succeeds, the success might not correspond to a real proof. Deletion of facts from a database is a good example of a nonlogical operation. Regular intuitionistic and classical logic is monotonic: deduction from premises can only learn new facts, it can never disprove things you already knew to be true. Since deletion removes facts from the set of things you know, it can't have a logical interpretation in classical/intuitionistic logic.

However, it turns out that not all logics are monotonic, and in this paper Simmons and Pfenning show that if you take the language of propositions to be a fragment of linear logic, then all of the operations that Ganzinger and McAllester use actually do have a nice logical interpretation.