Some recent theoretical work in proof search has illustrated that it is possible to combine the following two computational principles into one computational logic:
All these features have a clean proof theory. The combination of these features allow, for example, specifying rather declarative approaches to model checking syntactic expressions containing bindings. The Bedwyr system is intended as an implementation of these computational logic principles.
In the legend of King Arthur and the round table, several knights shared in the search for the holy grail. The name of one of them, Parsifal, is used for an INRIA team where Bedwyr is currently developed. Bedwyr was another one of those knights. Wikipedia (using the spelling “Bedivere”) mentions that Bedwyr appears in Monty Python and the Holy Grail where he is “portrayed as a master of the extremely odd logic of ancient times”. Bedwyr is a re-implementation and rethinking of an earlier system called Level 0/1 written by Alwen Tiu and described in [TNM05]. It was an initial offering from “Slimmer”, a jointly funded effort between INRIA and the University of Minnesota on “Sophisticated logic implementations for modeling and mechanical reasoning” from 2005 to 2010. For more information, see http://slimmer.gforge.inria.fr/.
The term “higher-order abstract syntax” (hoas) was originally coined by Pfenning and Elliott in [PE88] and names the general practice (that was common then in, say, λProlog [MN87]) of using an abstraction in a programming or specification language to encode binders in an object-language. Since the choice of “meta-language” can vary a great deal, the term “hoas” has come to mean different things to different people. When hoas is used directly within functional programming or constructive type systems, syntax with bindings contains functional objects, which make rich syntactic manipulations difficult. Bedwyr, on the other hand, follows the λ-tree approach [Mil00] to hoas: in particular, Bedwyr’s use of λ-abstraction is meant to provide an abstract form of syntax in which only the names of bindings are hidden: the rest of the structure of syntactic expressions remains.
Some care has been taken to implement the novel logical principles that appear in Bedwyr. In particular, the system makes extensive use of the implementation of the suspension calculus [Nad99] and other implementation ideas developed within the Teyjus [NM99] implementation of λProlog [NM88]. Aspects of tabled deduction have also been added to the system [RRR+97, Pie05]. We have found that Bedwyr’s performance is good enough to explore a number of interesting examples. It is not likely, however, that the current implementation will support large examples. For example, the system implements the occur-check within logic: this is, of course, necessary for sound deduction but it does slow unification a lot. As a result, the append program is quadratic in the size of its first argument. There are a number of well-known improvements to unification that make it possible to remove many instances of the occur-check (and making append linear). As of this time, such an improvement has not been added to Bedwyr.
The Bedwyr system was conceived as a prototype that could help validate certain proof theory and proof search topic. In the end, this prototype has illustrated the main principles that we hoped that it would. It has also pointed out a number of new topics to be explored. If you are interested in contributing examples, features, or performance enhancements, or if you are interested in considering the next generation of a system like this, please let an author of this guide know: we are looking for contributions.
To read this guide, we shall assume that the reader is familiar with the implementation of proof search that is found in, say, Prolog, λProlog, or Twelf. While familiarity with various foundations-oriented papers (particularly, [MMP03, MT05, Tiu04, Bae08b, TM10]) is important for understanding fully this system, much can be learned from studying the examples provided in the distribution.