A logical framework is a general meta-language for specifying and implementing deductive systems, given by axioms and inference rules. Recently, one major application of logical frameworks has been in the area of ``certified code''. To provide guarantees about the behavior of mobile code, safety properties are expressed as deductive systems. The code producer then verifies the program according to some predetermined safety policy, and supplies a binary executable together with its safety proof (certificate). Before executing the program, the host machine then quickly checks the code's safety proof against the binary. The safety policy and the safety proofs can be expressed in the logical framework thereby providing a general safety infrastructure. Moreover, it is possible to experiment with safety policies and verify that the program is in fact safe by executing the safety policy using a logic programming interpretation.
The Twelf system [22] is an implementation of a logical framework based on the dependently typed lambda calculus [8]. By assigning an operational interpretation to types, we obtain a higher-order logic programming language [19]. Higher-order logic programming extends traditional first-order logic programming in three ways: First, we have a rich type system based on dependent types, which allows the user to define her own higher-order data-types and supports higher-order abstract syntax [21]. Second, we not only have a static set of program clauses, but assumptions may be introduced dynamically during proof search. Third, we have an explicit notion of proof, i.e. the logic programming interpreter does not only return an answer substitution for the free variables in the query, but the actual proof as a term in the dependently typed lambda-calculus.
The Twelf system has been used in several projects on certified code [4,5,3]. The code size in the foundational proof-carrying code project [1] at Princeton ranges between 70,000 and 100,000 lines of Twelf code, which includes data-type definitions and proofs. The higher-order logic program, which is used to execute safety policies, consists of over 5,000 lines of code, and over 600 - 700 clauses. Such large specifications have put to test implementations of logical frameworks and exposed several problems: First, performance may be severely hampered by redundant computation, leading to long response times and slow development of formal specifications. Second, many straightforward specifications of formal systems, for example recognizers and parsers for grammars, rewriting systems, type systems with subtyping or polymorphism, are not executable, thus requiring more complex and sometimes less efficient implementations.
Here we describe three techniques to overcome some of the existing
performance barriers and extend its expressive power. This summarizes
some recent work which was carried out as part of the Twelf project at
Carnegie Mellon University. First, we describe the central idea behind
optimizing unification in logical frameworks by eliminating
unnecessary occurs-checks. Second we present a novel execution model
for higher-order logic programming based on selective memoization and
third we will discuss higher-order term indexing techniques to sustain
performance in large-scale examples. Experiments carried out in Twelf
demonstrate, these optimizations taken together constitute a
significant step toward exploring the full potential of logical
frameworks in real-world applications. Although the main focus of this
work has been the logical framework Twelf, we believe the presented
optimizations are applicable to any higher-order reasoning system such
as Lambda Prolog
[13] or Isabelle
[18].
The most comprehensive study on efficient and robust implementation techniques for higher-order unification so far has been carried out by Nadathur and colleagues for the simply-typed lambda-calculus in the programming language Lambda Prolog [14]. Higher-order unification is implemented via Huet's algorithm [9] and special mechanisms are incorporated into the WAM instruction set to support branching and postponing unification problems. To only perform an occurs-check when necessary, the compiler distinguishes between the first occurrence and subsequent occurrences of a variable and compiles them into different WAM instructions. While for the first occurrence of a variable the occurs-check may be omitted, full unification is used for all subsequent variables. This approach seems to work well in the simply-typed setting, however it is not clear how to generalize it to dependent types. In addition, it is well known, that Huet's algorithm is highly non-deterministic and requires backtracking. An important step toward efficient implementations, has been the development of higher-order pattern unification [11,20]. For this fragment, higher-order unification is decidable and deterministic. As was shown in [10], most programs written in practice fall into this fragment. Unfortunately, the complexity of this algorithm is still at best linear [27] in the sum of the sizes of the terms being unified, which is impractical for any useful programming language or practical framework.
In [26], the author
and Pfenning present an abstract view of existential variables in the
dependently typed lambda-calculus based on modal type theory. This
allows us to distinguish between existential variables, which are
represented as modal variables, and bound variables, which are
described by ordinary variables. This leads to a simple clean
framework which allows us to explain a number of features of the
current implementation of higher-order unification in Twelf
[22] and provides insight
into several optimizations such as lowering and raising. In
particular, it explains one optimization called linearization, which
eliminates many unnecessary occurs-checks. Terms are compiled into
linear higher-order patterns and some additional variable
definitions. Linear higher-order patterns restrict higher-order
patterns in two ways: First, all existential variables occur only
once. Second, we impose some further syntactic restrictions on
existential variables, i.e. they must be applied to all
distinct bound variables. This is in contrast to higher-order
patterns, which only require that existential variables are applied to
some bound variables. Linear higher-order patterns can be
solved with an assignment algorithm which resembles first-order
unification (without the occurs check) closely and is constant time.
Experimental results show that a large class of programs falls into
the linear higher-order pattern fragment and can be handled with this
algorithm. This leads to significant performance improvement (up to a
factor of 5) in many example applications including those in the area
of proof-carrying code.
The success of memoization in first-order logic programming strongly suggests that memoization may also be valuable in higher-order logic programming. In fact, Necula and Lee point out in [16] that typical safety proofs in the context of certified code commonly have repeated sub-proofs that should be hoisted out and proved only once. Memoization has potentially three advantages. First, proof search is faster thereby substantially reducing the response time to the programmer. Second, the proofs themselves are more compact and smaller. This is especially important in applications to secure mobile code where a proof is attached to a program, as smaller proofs take up less time to check and transmit to another host. Third, substantially more specifications, for example recognizers and parser for grammars, evaluators based on rewriting or type systems with subtyping, are executable under the new paradigm thereby extending the power of the existing system.
Using memoization in higher-order logic programming poses several challenges, since we have to handle type dependencies and may have dynamic assumptions which are introduced during proof search. This is unlike tabling in XSB, where we have no types and it suffices to memoize atomic goals. Moreover, most descriptions of tabling in the first-order setting are closely oriented on the WAM (Warren Abstract Machine) making it hard to transfer tabling techniques and design extensions to other logic programming interpreters.
In [24], we have presented a characterization of tabled higher-order logic programing based on uniform proofs [12]. This abstract view provides a high-level description of a tabled logic programming interpreter and separates logical issues from procedural ones leaving maximum freedom to choose particular control mechanisms. It also facilitates applying memoization to other logic programming environments such as Lambda Prolog [13] or using memoization in Isabelle [18].
We have implemented the search strategy based on memoization for the
Twelf system and have conducted several experiments with parser and
recognizers for grammars, refinement type systems, and reduction
semantics for functional programs, rewriting systems for the
lambda-calculus etc
[23]. Experimental results
demonstrate that memoization not only allows us to execute more
specifications, but also execute them more efficiently. Since
computation based on memoization terminates for programs with
bounded-term size property and it is a complete search strategy, we
also get better and more useful failure behavior. We see this work is
an important step toward a practical programming environment for
developing and prototyping safety policies and deductive systems in
general.
We have designed and implemented higher-order term indexing techniques based on substitution trees [25]. Substitution tree indexing is a highly successful technique in first-order theorem proving, which allows the sharing of common sub-expressions via substitutions. This work extends first-order substitution tree indexing [7] to the higher-order setting.
Given two terms pred (h (h b)) (g b) b and
We can obtain the first term by composing all the substitutions in the left-most path.
This poses several challenges: First of all, building a substitution
tree relies on computing the most specific generalization of two
terms. However in the higher-order setting, the most specific
generalization of two terms may not exist in general. Second,
retrieving all terms, which unify or match, needs to be efficient -
but higher-order unification is undecidable in general. Although, most
specific generalizations exist for higher-order patterns and decidable
higher-order pattern unification
[11,20], these algorithms may not
be efficient in practice
[26]. Therefore, it
is not obvious that they are suitable for higher-order term indexing
techniques. Instead, we use linear higher-order patterns as a basis
for higher-order term indexing
[26]. This allows us
to reduce the problem of computing most specific generalizations for
higher-order terms to an algorithm which resembles closely its
first-order counterpart
[25]. This technique has
been implemented to speed-up the execution of the tabled higher-order
logic programming engine in Twelf. Experimental results demonstrate
that higher-order term indexing leads to substantial performance
improvements (by up to a factor of 10), illustrating the importance
of indexing in general
[25].
We presented several techniques which considerably improve the performance of higher-order reasoning systems. This a first step toward exploring the full potential of logical frameworks in practice and apply it to new areas such as security and authentication [2]. However, the presented techniques are just a first step toward narrowing the performance gap between higher-order and first-order systems. There are many more optimizations which have been already proven successful in the first-order setting and we may be able to apply to higher-order languages. For example, term indexing may not only be used for managing the memo-tables, but also be apply to indexing program clauses. There are also new considerations due to the dependently typed setting. For example, typing information needs to be carried around during run-time and leads to redundancies in the representation of terms. A first step toward eliminating this kind of redundancy has been proposed by Necula and Lee [17] for a fragment of the logical framework. Finally, the application of logical frameworks to certified code raises new question, which traditionally have not played a central role in logic programming. The central idea in certified code is not only to verify that a program is safe, but also to efficiently transmit and then check the proof. Necula and Rahul [15] explored the novel use of higher-order logic programming for checking the correctness of a certificate. In their case, the certificate is a bit-string which encodes the non-deterministic choices of a proof and can be used to guide a logic programming interpreter. Hence, a proof can be checked by guiding the higher-order logic programming interpreter with the bit-string and reconstructing the actual proof. Here, memoization can be used to factor out common sub-proofs and eliminate the checking of redundant sub-proofs.