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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Has anyone ever given a

Has anyone ever given a serious comparison of Qi and Coq? My impression so far is that Qi makes the usual mistake of relying on too many orthogonal mechanisms, probably because the creator is not familiar with the simple foundations behind Coq, Agda, Epigram, and relatives.

can you say more?

i haven't used Qi or Coq other than very briefly, but am interested in them. might you point to a discussion of the issue of too much orthogonality? (i would guess it has to do with things becoming difficult from a usability perspective in the end.) thank you.

Book online

The book, Functional Programming in Qi, is available online now.