BRICS RS-04-5 Dariusz & Olivier: From Interpreter to Logic Engine by Defunctionalization BRICS

Basic Research in Computer Science

From Interpreter to Logic Engine by Defunctionalization

Biernacki Dariusz Danvy Olivier BRICS Report Series RS-04-5 ISSN 0909-0878 March 2004 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2004, Biernacki Dariusz & Danvy Olivier.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/04/5/

From Interpreter to Logic Engine by Defunctionalization ^{∗}

Dariusz Biernacki and Olivier Danvy BRICS^{†} Department of Computer Science University of Aarhus^{‡}

March 1, 2004

Abstract

Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds’s defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.

∗To appear in the proceedings of LOPSTR 2003.

† Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

‡ IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark.

Email: {dabi,danvy}@brics.dk

Contents

1 Introduction 3 1.1 A simple example of defunctionalization . . . . . . . . . . . . . . 3 1.2 A more advanced example: the factorial function . . . . . . . . . 4

2 Propositional Prolog 6

3 A generic interpreter for propositional Prolog 7 3.1 A generic notion of answers and results . . . . . . . . . . . . . . 7 3.2 Specific answers and results . . . . . . . . . . . . . . . . . . . . . 7

3.2.1 The first solution . . . . . . . . . . . . . . . . . . . . . . . 7 3.2.2 The number of solutions . . . . . . . . . . . . . . . . . . . 8

3.3 The generic interpreter, semi-compositionally . . . . . . . . . . . 8 3.4 Specific interpreters . . . . . . . . . . . . . . . . . . . . . . . . . 10

3.4.1 A specific interpreter computing the first solution . . . . . 10 3.4.2 A specific interpreter computing the number of solutions . 10

4 Two abstract machines for propositional Prolog 11 4.1 The first solution . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.2 The number of solutions . . . . . . . . . . . . . . . . . . . . . . . 11

5 Related work and conclusion 14

A A direct-style interpreter for Prolog 15

1 Introduction

In previous work [2], we presented a derivation from interpreter to abstract machine that makes it possible to connect known λ-calculus interpreters to known abstract machines for the λ-calculus, as well as to discover new ones. The goal of this work is to test this derivation on a programming language other than the λ-calculus. Our pick here is a simple logic programming language, propositional Prolog with cut (Section 2). We present its abstract syntax, informal semantics, and computational model, which we base on success and failure continuations (Section 3). We then specify an interpreter for propositional Prolog in a generic and parameterized way that leads us to a logic engine. This logic engine is a transition system that we obtain by defunctionalizing the success and failure continuations (Section 4). We also present and analyze a direct-style interpreter for propositional Prolog (Appendix A).

The abstract machines we consider are models of computation rather than devices for high performance, and the transformations we consider are changes of representation rather than optimizations.

Prerequisites: We expect a passing familiarity with the notions of success and failure continuations as well as with Standard ML and its module language.

As for defunctionalization, it originates in Reynolds’s seminal article on definitional interpreters for higher-order programming languages [27]. The point of defunctionalization is to transform a higher-order program into a first-order program by replacing its function types by sum types. Before defunctionalization, the inhabitants of each function type are instances of anonymous lambda-abstractions. Defunctionalizing a program amounts to enumerating these lambda-abstractions in a sum type: each function introduction (i.e., lambdaabstraction) is replaced by the corresponding constructor holding the values of the free variables of this lambda-abstraction, and each function elimination (i.e., application) is replaced by a case dispatch. After defunctionalization, the inhabitants of each function type are represented by elements of a corresponding sum type.

Danvy and Nielsen’s study of defunctionalization contains many examples [14], but to make the present article self-contained, let us consider two concrete cases.

1.1 A simple example of defunctionalization

The following (trivial) program is higher-order because of the auxiliary function aux, which is passed a function of type int -> int as argument:

     (*  aux : int * (int -> int) -> int  *)
     fun aux (x, f)
         = (f 10) + (f x)
     (*  main : int * int * int -> int  *)
     fun main (a, b, c)
         = (aux (a, fn x => x + b)) * (aux (c, fn x => x * x))

The inhabitants of the function space int -> int are instances of the two anonymous lambda-abstractions declared in main, fn x => x + b and fn x => x * x. The first one has one free variable (b, of type int), and the second one is closed, i.e., it has no free variables.

To defunctionalize this program, we enumerate these lambda-abstractions in a sum type lam, and we define the corresponding apply function to interpret each of the summands:

     datatype lam = LAM1 of int
                  | LAM2
     (*  apply_lam : lam * int -> int  *)
     fun apply_lam (LAM1 b, x)
         = x + b
       | apply_lam (LAM2, x)
         = x * x

In the defunctionalized program, each lambda-abstraction is replaced by the corresponding constructor, and each application is replaced by a call to the apply function:

     (*  aux : int * lam -> int  *)
     fun aux (x, f)
         = (apply_lam (f, 10)) + (apply_lam (f, x))
     (*  main : int * int * int -> int  *)
     fun main (a, b, c)
         = (aux (a, LAM1 b)) * (aux (c, LAM2))

The resulting program is first order.

1.2 A more advanced example: the factorial function

Let us defunctionalize the following continuation-passing version of the factorial function:

     (*  fac_c : int * (int -> 'a) -> 'a  *)
     fun fac_c (0, k)
         = k 1
       | fac_c (n, k)
         = fac_c (n - 1, fn v => k (n * v))
     (*  main : int -> int  *)
     fun main n
         = fac_c (n, fn v => v)

We consider the whole program (i.e., both main and fac c). Therefore the polymorphic type 'a, i.e., the domain of answers, is instantiated to int. The candidate function space for defunctionalization is that of the continuation, int -> int. Its inhabitants are instances of two lambda-abstractions: the initial continuation in main with no free variables, and the intermediate continuation in the induction case of fac c with two free variables: n and k. The corresponding data type has therefore two constructors:

     datatype cont = CONT0
                   | CONT1 of int * cont
     (*  apply_cont : cont * int -> int  *)
     fun apply_cont (CONT0, v)
         = v
       | apply_cont (CONT1 (n, k), v)
         = apply_cont (k, n * v)

Correspondingly, the apply function associated to the data type interprets each of these constructors according to the initial continuation and the intermediate continuation.

We observe that cont is isomorphic to the data type of lists of integers. We therefore adopt this simpler representation of defunctionalized continuations:

     type cont = int list
     (*  apply_cont : cont * int -> int  *)
     fun apply_cont (nil, v)
         = v
       | apply_cont (n :: k, v)
         = apply_cont (k, n * v)

In the defunctionalized program, the continuations are replaced by the constructors, and the applications of the continuations are replaced by a call to

apply cont:
     (*  fac_c : int * cont -> int  *)
     fun fac_c (0, k)
         = apply_cont (k, 1)
       | fac_c (n, k)
         = fac_c (n - 1, n :: k)
     (*  main : int -> int  *)
     fun main n
         = fac_c (n, nil)

The resulting program is first-order, all its calls are tail calls, and all computations in the actual parameters are elementary. It is therefore a transition system in the sense of automata and formal languages [23]. Both main and fac c, together with their actual parameters, form configurations and their ML definitions specify a transition relation, as expressed in the following table. The top transition specifies the initial state and the bottom transition specifies the terminating configurations. The machine consists of two mutually recursive transition functions; the first one operates over pairs of integers, and the second one operates over a stack of integers and an integer:

n ⇒ ⟨n, nil⟩_{fac}
⟨0, k⟩_{fac} ⇒ ⟨k, 1⟩_{app}
⟨n, k⟩_{fac} ⇒ ⟨n − 1, n :: k⟩_{fac}
⟨n :: k, v⟩_{app} ⇒ ⟨k, n × v⟩_{app}
⟨nil, v⟩_{app} ⇒ v

Accordingly, the result of defunctionalizing a continuation-passing interpreter is also a transition system, i.e., an abstract machine in the sense of automata and formal languages [23]. We used this property in our work on the λ-calculus [2], and we use it here for propositional Prolog.

2 Propositional Prolog

The abstract syntax of propositional Prolog reads as follows:

     structure Source
     = struct
         type ide = string
         datatype atom = IDE of ide
                       | OR of goal * goal
                       | CUT
                       | FAIL
         withtype goal = atom list
         type clause = ide * goal
         datatype program = PROGRAM of clause list
         datatype top_level_goal = GOAL of goal
       end

A program consists of a list of clauses. A clause consists of an identifier (the head of the clause) and a goal (the body of the clause). A goal is a list of atoms; an empty list represents the logical value ‘true’ and a non-empty list of atoms represents their conjunction. Each atom is either an identifier, the disjunction of two goals, the cut operator, or the fail operator.

The intuitive semantics of the language is standard. Given a Prolog program and a goal, we try to verify whether the goal follows from the program in the sense of propositional logic, i.e., in terms of logic programming, whether the SLD-resolution algorithm for this goal and this program stops with the empty clause. If it does, then the answer is positive; if it stops with one or more subgoals still waiting resolution, then the answer is negative. Here the unification algorithm consists in looking up the clause with a specified head in the program.

An atom can be a disjunction of two goals, and therefore if a chosen body does not lead to the positive answer, the other disjunct is tried, using backtracking. Backtracking can also be used to find all possible solutions in the resolution tree, which in case of propositional Prolog amounts to counting the positive answers. Two operators provide additional control over the traversal of the resolution tree: the cut operator removes some of the potential paths and the fail operator makes the current goal unsatisfiable, which triggers backtracking.

3 A generic interpreter for propositional Prolog

To account for the backtracking necessary to implement resolution, we use success and failure continuations [13]. A failure continuation is a parameterless function (i.e., a thunk) yielding a final answer. A success continuation maps a failure continuation to a final answer. The initial success continuation is applied if a solution has been found. The initial failure continuation is applied if no solution has been found. In addition, to account for the cut operator, we pass a cut continuation, i.e., a cached failure continuation. As usual with continuations, the domain of answers is left unspecified.

3.1 A generic notion of answers and results

We specify answers with an ML signature. The type of answers comes together with an initial success continuation and an initial failure continuation. The signature also declares a type of results and an extraction function mapping a (generic) answer to a (specific) result.

     signature ANSWER
     = sig
         type answer
         val sc_init : (unit -> answer) -> answer
         val fc_init : unit -> answer
         type result
         val extract : answer -> result
       end

3.2 Specific answers and results

We consider two kinds of answers: the first solution, if any, and the total number of solutions.

3.2.1 The first solution

This notion of answer is the simplest to define. Both answer and result are defined as the type of booleans and extract is the identity function. The initial success continuation ignores the failure continuation and yields true, whereas the initial failure continuation yields false.

     structure Answer_first : ANSWER
     = struct
         type answer = bool
         fun sc_init fc = true
         fun fc_init () = false
         type result = bool
         fun extract a = a
       end

3.2.2 The number of solutions

This notion of answer is more delicate. One could be tempted to define answer as the type of integers, but the resulting implementation would no longer be tail recursive.^{1} Instead, we use an extra layer of continuations: We define answer as the type of functions from integers to integers, result as the type of integers, and extract as a function triggering the whole resolution by applying an answer to the initial count, 0. The initial success continuation takes note of an intermediate success by incrementing the current count and activating the failure continuation. The initial failure continuation is passed the final count and returns it.

     structure Answer_how_many : ANSWER
     = struct
         type answer = int -> int
         fun sc_init fc = (fn m => fc () (m+1))
         fun fc_init () = (fn m => m)
         type result = int
         fun extract a = a 0
       end

3.3 The generic interpreter, semi-compositionally

We define a generic interpreter for propositional Prolog, displayed in Figure 1, as a recursive descent over the source syntax, parameterized by a notion of answers, and implementing the following signature:

     signature INTERPRETER
     = sig
         type result
         val main : Source.top_level_goal * Source.program -> result
       end

In run goal, an empty list of atoms is interpreted as ‘true’, and accordingly, the success continuation is activated. A non-empty list of atoms is sequentially interpreted by run seq by extending the success continuation; this interpretation

1In “fun sc init fc = 1 + (fc ())”, the call to fc is not a tail call.

functor mkInterpreter (structure A : ANSWER) : INTERPRETER
= struct
open Source
type result = A.result
type fcont = unit -> A.answer
type scont = fcont -> A.answer
type ccont = fcont
(*  run_goal : goal * clause list * scont * fcont * ccont -> A.answer  *)
fun run_goal (nil, p, sc, fc, cc)
    = sc fc
  | run_goal (a :: g, p, sc, fc, cc)
    = run_seq (a, g, p, sc, fc, cc)
(*  run_seq : atom * goal * clause list * scont * fcont * ccont
              -> A.answer  *)
and run_seq (a, nil, p, sc, fc, cc)
    = run_atom (a, p, sc, fc, cc)
  | run_seq (a, a' :: g, p, sc, fc, cc)
    = run_atom (a, p, fn fc' => run_seq (a', g, p, sc, fc', cc), fc, cc)
(*  run_atom : atom * clause list * scont * fcont * ccont -> A.answer  *)
and run_atom (IDE i, p, sc, fc, cc)
    = (case lookup (i, p)
         of NONE
            => fc ()
          | (SOME g)
            => run_goal (g, p, sc, fc, fc))
  | run_atom (OR (g1, g2), p, sc, fc, cc)
    = run_goal (g1, p, sc, fn () => run_goal (g2, p, sc, fc, cc), cc)
  | run_atom (CUT, p, sc, fc, cc)
    = sc cc
  | run_atom (FAIL, p, sc, fc, cc)
    = fc ()
(*  main : top_level_goal * program -> A.result  *)
fun main (GOAL g, PROGRAM p)
    = let val a = run_goal (g, p, A.sc_init, A.fc_init, A.fc_init)
      in A.extract a
      end
end

Figure 1: A generic interpreter for propositional Prolog singles out the last atom in a properly tail-recursive manner. An identifier is interpreted either by failing if it is not the head of any clause in the program, or by resolving the corresponding goal with the cut continuation replaced with the current failure continuation. The function lookup searching for a clause with a given head reads as follows:

     (*  lookup : Source.ide * Source.clause list -> Source.goal option  *)
     fun lookup (i, p)
         = let fun walk nil
                   = NONE
                 | walk ((i', g) :: p)
                   = if i = i'
                     then SOME g
                     else walk p
           in walk p
           end

A disjunction of two goals is interpreted by extending the failure continuation. The cut operator is interpreted by replacing the failure continuation with the cut continuation. The fail operator is interpreted as ‘false’, and accordingly, the failure continuation is activated.

This interpreter is not compositional (in the sense of denotational semantics) because g, in the interpretation of identifiers, does not denote a proper subpart of the denotation of l. The interpreter, however, is semi-compositional in Jones’s sense [19, 20], i.e., g denotes a proper subpart of the source program. (To make the interpreter compositional, one can follow the tradition of denotational semantics and use an environment mapping an identifier to a function that either evaluates the goal denoted by the identifier or calls the failure continuation. The environment is threaded in the interpreter instead of the program. The resulting ML interpreter represents the valuation function of a denotational semantics of propositional Prolog.)

3.4 Specific interpreters

3.4.1 A specific interpreter computing the first solution

A specific interpreter computing the first solution, if any, is obtained by instantiating mkInterpreter with the corresponding notion of answers:

   structure Prolog first = mkInterpreter (structure A = Answer first)

3.4.2 A specific interpreter computing the number of solutions

A specific interpreter computing the number of solutions is also obtained by instantiating mkInterpreter with the corresponding notion of answers:

 structure Prolog how many = mkInterpreter (structure A = Answer how many)

Appendix A contains a direct-style counterpart of the interpreter (uncurried and without cut) computing the number of solutions.

4 Two abstract machines for propositional Prolog

We successively consider each of the specific Prolog interpreters of Section 3.4 and we defunctionalize their continuations. As already illustrated in Section 1 with the factorial program, in each case, the result is an abstract machine. Indeed the interpreters are in continuation-passing style, and thus:

• all their calls are tail calls, and therefore they can run iteratively; and

• all their subcomputations (i.e., the computation of their actual parameters) are elementary.

In both cases the types of the defunctionalized success and failure continuations read as follows:

     datatype scont = SCONT0
                    | SCONT1 of atom * goal * clause list * scont * ccont
          and fcont = FCONT0
                    | FCONT1 of goal * clause list * scont * fcont * ccont
     withtype ccont = fcont

As in Section 1.2, since both data types are isomorphic to the data type of lists, we represent them as such when presenting the abstract machines.

4.1 The first solution

The abstract machine is defined as the transition system shown in Figure 2. The top part specifies the initial state and the bottom part specifies the terminating configurations. The machine consists of three mutually recursive transition functions, two of which operate over a quintuple and one over a six-element tuple. The quintuple consists of the goal, the program, the (defunctionalized) success continuation, the (defunctionalized) failure continuation and the cut continuation (a register caching a previous failure continuation). The six-element tuple additionally has the first atom of the goal as its first element.

4.2 The number of solutions

This abstract machine is displayed in Figure 3 and is similar to the previous one, but operates over a six- and seven-element tuples. The extra component is the counter.

Both machines are deterministic because they were derived from (deterministic) functions.

• Atoms, goals and programs:

a ::= IDE i | OR (g_{1} , g_{2} ) | CUT | FAIL
g ::= a^{∗}
p ::= (i, g)^{∗}

• Control stacks:

sc ::= nil | (a, g, p, cc) :: sc
fc ::= nil | (g, p, sc, cc) :: fc
cc ::= fc

• Initial transition, transition rules and final transition:

⟨g, p⟩ ⇒ ⟨g, p, nil, nil, nil⟩_{goal}

⟨nil, p, (a, g, p′, cc′) :: sc, fc, cc⟩_{goal} ⇒ ⟨a, g, p′, sc, fc, cc′⟩_{seq} ⟨a :: g, p, sc, fc, cc⟩_{goal} ⇒ ⟨a, g, p, sc, fc, cc⟩_{seq} ⟨a, nil, p, sc, fc, cc⟩_{seq} ⇒ ⟨a, p, sc, fc, cc⟩_{atom}

⟨a, a′ :: g, p, sc, fc, cc⟩_{seq} ⇒ ⟨a, p, (a′, g, p, cc) :: sc, fc, cc⟩_{atom}

⟨IDE i, p, sc, fc, cc⟩_{atom} ⇒ ⟨g, p, sc, fc, fc⟩_{goal}

if lookup (i) succeeds with g

⟨IDE i, p, sc, (g, p, sc′, cc′) :: fc, cc⟩_{atom} ⇒ ⟨g, p′, sc′, fc, cc′⟩_{goal}

if lookup (i) fails

⟨OR (g_{1} , g_{2} ), p, sc, fc, cc⟩_{atom} ⇒ ⟨g_{1} , p, sc, (g_{2} , p, sc, cc) :: fc, cc⟩_{goal} ⟨CUT, p, (a, g, p′, cc′) :: sc, fc, cc⟩_{atom} ⇒ ⟨a, g, p′, sc, fc, cc′⟩_{seq}

⟨FAIL, p, sc, (g, p′, sc′, cc′) :: fc, cc⟩_{atom} ⇒ ⟨g, p′, sc′, fc, cc′⟩_{goal} ⟨nil, p, nil, fc, cc⟩_{goal} ⇒

true

⟨IDE i, p, sc, nil, cc⟩_{atom} ⇒ false, if lookup (i) fails ⟨FAIL, p, sc, nil, cc⟩_{atom} ⇒

false

⟨CUT, p, nil, fc, cc⟩_{atom} ⇒

true

Figure 2: An abstract machine computing the first solution • Atoms, goals and programs:

a ::= IDE i | OR (g_{1} , g_{2} ) | CUT | FAIL
g ::= a^{∗}
p ::= (i, g)^{∗}

• Control stacks:

sc ::= nil | (a, g, p, cc) :: sc
fc ::= nil | (g, p, sc, cc) :: fc
cc ::= fc

• Initial transition, transition rules and final transition:

⟨g, p⟩ ⇒ ⟨g, p, nil, nil, nil, 0⟩_{goal}

⟨nil, p, nil, (g, p′, sc, cc′) :: fc, cc, m⟩_{goal} ⇒ ⟨g, p′, sc, fc, cc′, m + 1⟩_{goal} ⟨nil, p, (a, g, p′, cc′) :: sc, fc, cc, m⟩_{goal} ⇒ ⟨a, g, p′, sc, fc, cc′, m⟩_{seq}

⟨a :: g, p, sc, fc, cc, m⟩_{goal} ⇒ ⟨a, g, p, sc, fc, cc, m⟩_{seq} ⟨a, nil, p, sc, fc, cc, m⟩_{seq} ⇒ ⟨a, p, sc, fc, cc, m⟩_{atom}

⟨a, a′ :: g, p, sc, fc, cc, m⟩_{seq} ⇒ ⟨a, p, (a′, g, p, cc) :: sc, fc, cc, m⟩_{atom}

⟨IDE i, p, sc, fc, cc, m⟩_{atom} ⇒ ⟨g, p, sc, fc, fc, m⟩_{goal} if lookup (i) succeeds with g

⟨IDE i, p, sc, (g, p, sc′, cc′) :: fc, cc, m⟩_{atom} ⇒ ⟨g, p′, sc′, fc, cc′, m⟩_{goal}

if lookup (i) fails

⟨OR (g_{1} , g_{2} ), p, sc, fc, cc, m⟩_{atom} ⇒ ⟨g_{1} , p, sc, (g_{2} , p, sc, cc) :: fc, cc, m⟩_{goal}

⟨CUT, p, (a, g, p′, cc′) :: sc, fc, cc, m⟩_{atom} ⇒ ⟨a, g, p′, sc, fc, cc′, m⟩_{seq} ⟨CUT, p, nil, (g, p′, sc, cc′) :: fc, cc, m⟩_{atom} ⇒ ⟨g, p′, sc, fc, cc′, m + 1⟩_{goal} ⟨FAIL, p, sc, (g, p′, sc′, cc′) :: fc, cc, m⟩_{atom} ⇒ ⟨g, p′, sc′, fc, cc′, m⟩_{goal}

⟨nil, p, nil, nil, cc, m⟩_{goal} ⇒

m + 1

⟨FAIL, p, sc, nil, cc, m⟩_{atom} ⇒ m ⟨CUT, p, nil, nil, cc, m⟩_{atom} ⇒

m + 1

⟨IDE i, p, sc, nil, cc, m⟩_{atom} ⇒ m, if lookup (i) fails

Figure 3: An abstract machine computing the number of solutions

5 Related work and conclusion

In previous work [2, 3, 10], we presented a derivation from interpreter to abstract machine, and we were curious to see it applied to something else than a functional programming language. The present paper reports its application to a logic programming language, propositional Prolog. In its entirety, the derivation consists of closure conversion, transformation into continuationpassing style (CPS), and defunctionalization. Closure conversion ensures that any higher-order values are made first-order.^{2} The CPS transformation makes the flow of control of the interpreter manifest as a continuation. Defunctionalization materializes the flow of control as a first-order data structure. In the present case, propositional Prolog is a first-order language and the interpreter we consider is already in continuation-passing style (cf. Appendix A). Therefore the derivation reduces to defunctionalization. The result is a simple logic engine, i.e., mutually recursive and first-order transition functions. It was derived, not invented, and so, for example, its two stacks arise as defunctionalized continuations. Similarly, it is properly tail recursive since the interpreter is already properly tail recursive.

Since the correctness of defunctionalization has been established [5, 26], the correctness of the logic engine is a corollary of the correctness of the original interpreter.

Prolog has both been specified and formalized functionally. For example, Carlsson has shown how to implement Prolog in a functional language [7]. Continuation-based semantics of Prolog have been studied by de Bruin and de Vink [15] as well as by Nicholson and Foo [25]. Our closest related work is de Bruin and de Vink’s continuation semantics for Prolog with cut:

• de Bruin and de Vink present a denotational semantics with success and failure continuations; their semantics is (of course) compositional, and comparable to the compositional interpreter outlined in Section 3.3. The only difference is that their success continuations expect both a failure continuation and a cut continuation, whereas our success continuations expect only a failure continuation. Analyzing the control flow of the corresponding interpreter, we have observed that the cut continuation is the same at the definition point and at the use point of a success continuation. Therefore, there is actually no need to pass cut continuations to success continuations.

• de Bruin and de Vink also present an operational semantics, and prove it equivalent to their denotational semantics. In contrast, we defunctionalized the interpreter corresponding to a denotational semantics into an interpreter corresponding to an operational semantics. We also “refunctionalized” the interpreter corresponding to de Bruin and de Vink’s operational semantics, and we observed that in the resulting interpreter (which corresponds to a denotational semantics), success continuations are not passed cut continuations.

2Closures, for example, are used to implement higher-order logic programming [8].

Designing abstract machines is a favorite among functional programmers [16]. Unsurprisingly, this is also the case among logic programmers, for example, with Warren’s abstract machine [4], which incidentally is more of a device for high performance than a model of computation. Just as unsurprisingly, functional programmers use functional programming languages as their meta-language and logic programmers use logic programming languages as their meta-language. For example, Kursawe showed how to “invent” Prolog machines out of logicprogramming considerations [22]. The goal of our work here was more modest: we simply aimed to test an interpreter-to-abstract-machine derivation that works well for the λ-calculus. The logic engine we obtained is basic but plausible. Its chief illustrative virtue is to show that the representation of a denotational semantics can be mechanically defunctionalized into the representation of an operational semantics (and, actually, vice versa). It also shows that proper tail recursion and the two control stacks did not need to be invented—they were already present in the original interpreter.

An alternative to deriving an abstract machine from an interpreter is to factor this interpreter into a compiler and a virtual machine, using, e.g., Wand’s combinator-based compiler derivation [29], Jørring and Scherlis’s staging transformations [21], Hannan’s pass-separation approach [18], or more generally the binding-time separation techniques of partial evaluation [20, 24]. We are currently experimenting with a such a factorization to stage our Prolog interpreter into a byte-code compiler and a virtual machine executing this byte code [1].

Acknowledgments: We are grateful to Mads Sig Ager, Małgorzata Biernacka, Jan Midtgaard, and the anonymous referees for their comments. This work is supported by the ESPRIT Working Group APPSEM II (http://www. appsem.org) and by the Danish Natural Science Research Council, Grant no. 21-03-0545.

A A direct-style interpreter for Prolog

The interpreter of Section 3 is in continuation-passing style to account for the backtracking necessary to implement resolution. Therefore, our derivation method which in its entirety consists of three steps—closure conversion, CPS transformation, and defunctionalization [2]—was reduced to only the last step. Less natural, but making the derivation closer to its original specification, would be to start it with an interpreter in direct style. The failure continuation could be eliminated by transforming the interpreter into direct style [9]. The success continuation, however, would remain. Because it is used non tail-recursively in the clause for disjunctions, it is what is technically called a delimited continuation (in contrast to the usual unlimited continuations of denotational semantics [28]).

structure Prolog_how_many_DS : INTERPRETER
= struct
open Source
type result = int
(*  run_goal : goal * clause list * int -> int  *)
fun run_goal (nil, p, m)
    = m
  | run_goal (a :: g, p, m)
    = run_seq (a, g, p, m)
(*  run_seq : atom * goal * clause list * int -> int  *)
and run_seq (a, nil, p, m)
    = run_atom (a, p, m)
  | run_seq (a, a' :: g, p, m)
    = let val m' = run_atom (a, p, m)
      in run_seq (a', g, p, m')
      end
(*  run_atom : atom * clause list * int -> int  *)
and run_atom (FAIL, p, m)
    = shift (fn sc => m)
  | run_atom (IDE i, p, m)
    = (case lookup (i, p)
         of NONE
            => shift (fn sc => m)
          | (SOME g)
            => run_goal (g, p, m))
  | run_atom (OR (g1, g2), p, m)
    = shift (fn sc => let val m' = sc (run_goal (g1, p, m))
                      in sc (run_goal (g2, p, m'))
                      end)
(*  main : top_level_goal * program -> int  *)
fun main (GOAL g, PROGRAM p)
    = reset (fn () => let val m = run_goal (g, p, 0)
                      in m + 1
                      end)
end

Figure 4: A direct-style interpreter for propositional Prolog Transforming the interpreter into direct style requires control operators for delimited continuations that are compatible with continuation-passing style, e.g., shift and reset [11, 12, 17].

Figure 4 presents such a direct-style interpreter for Propositional Prolog without cut, counting the number of solutions. CPS-transforming this interpreter once makes the success continuation appear. CPS-transforming the result makes the failure continuation appear, and yields the interpreter of Section 3.4.2 (minus cut). Defunctionalizing this interpreter yields the abstract machine of Section 4.2 (minus cut).

The reset control operator delimits control. Any subsequent use of the shift control operator will capture a delimited continuation that can be composed; this delimited continuation is the success continuation. Conjunction, in run seq, is implemented by function composition. Failure, in run atom, is implemented by capturing the current success continuation and not applying it. Disjunction, in run atom, is implemented by capturing the current success continuation and applying it twice. This interpreter is properly tail recursive, which is achieved by the two functions run goal and run seq that single out the last atom in a goal.

The interpreter is a new example of nondeterministic programming in direct style with control operators for the first level of the CPS hierarchy [6, 11]. In order to interpret the cut operator we would have to use the control operators of the second level, shift_{2} and reset_{2}.

References

[1] Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. From interpreter to compiler and virtual machine: a functional derivation. Technical Report BRICS RS-03-14, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, March 2003.

[2] Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Dale Miller, editor, Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’03), pages 8–19. ACM Press, August 2003.

[3] Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between call-by-need evaluators and lazy abstract machines. Technical Report BRICS RS-04-03, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, February 2004. Extended version of an article to appear in Information Processing Letters.

[4] Hassan Aït-Kaci. Warren’s Abstract Machine: A Tutorial Reconstruction. The MIT Press, 1991.

[5] Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Design and correctness of program transformations based on control-flow analysis. In Naoki Kobayashi and Benjamin C. Pierce, editors, Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, number 2215 in Lecture Notes in Computer Science, pages 420–447, Sendai, Japan, October 2001. Springer-Verlag.

[6] Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations. In Hayo Thielecke, editor, Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations, Technical report CSR-04-1, Department of Computer Science, Queen Mary’s College, pages 25–33, Venice, Italy, January 2004.

[7] Mats Carlsson. On implementing Prolog in functional programming. New Generation Computing, 2(4):347–359, 1984.

[8] Weidong Chen, Michael Kifer, and David S. Warren. Hilog: A foundation for higher-order logic programming. The Journal of Logic Programming, 15(3):187–230, February 1993.

[9] Olivier Danvy. Back to direct style. Science of Computer Programming, 22(3):183–195, 1994.

[10] Olivier Danvy. A rational deconstruction of Landin’s SECD machine. Technical Report BRICS RS-03-33, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, October 2003.

[11] Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151–160, Nice, France, June 1990. ACM Press.

[12] Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.

[13] Olivier Danvy, Bernd Grobauer, and Morten Rhiger. A unifying approach to goal-directed evaluation. New Generation Computing, 20(1):53–73, 2002. Extended version available as the technical report BRICS RS-01-29.

[14] Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. In Harald Søndergaard, editor, Proceedings of the Third International ACM SIG-PLAN Conference on Principles and Practice of Declarative Programming (PPDP’01), pages 162–174, Firenze, Italy, September 2001. ACM Press.

[15] Arie de Bruin and Erik P. de Vink. Continuation semantics for Prolog with cut. In Josep Díaz and Fernando Orejas, editors, TAPSOFT’89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, number 351 in Lecture Notes in Computer Science, pages 178–192, Barcelona, Spain, March 1989. Springer-Verlag.

[16] Stephan Diehl, Pieter Hartel, and Peter Sestoft. Abstract machines for programming language implementation. Future Generation Computer Systems, 16:739–751, 2000.

[17] Andrzej Filinski. Representing monads. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 446–457, Portland, Oregon, January 1994. ACM Press.

[18] John Hannan. Operational semantics directed machine architecture. ACM Transactions on Programming Languages and Systems, 16(4):1215–1247, 1994.

[19] Neil D. Jones. Computability and Complexity from a Programming Perspective. Foundations of Computing. The MIT Press, 1997.

[20] Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, London,

UK, 1993. Available online at http://www.dina.kvl.dk/\char'176sestoft/
pebook/.

[21] Ulrik Jørring and William L. Scherlis. Compilers and staging transformations. In Mark Scott Johnson and Ravi Sethi, editors, Proceedings of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 86–96, St. Petersburg, Florida, January 1986. ACM Press.

[22] Peter Kursawe. How to invent a Prolog machine. New Generation Computing, 5(1):97–114, 1987.

[23] John C. Martin. Introduction to Languages and the Theory of Computation. McGraw-Hill, 1991.

[24] Torben Æ. Mogensen. Separating binding times in language specifications. In Joseph E. Stoy, editor, Proceedings of the Fourth International Conference on Functional Programming and Computer Architecture, pages 14–25, London, England, September 1989. ACM Press.

[25] Tim Nicholson and Norman Y. Foo. A denotational semantics for Prolog. ACM Transactions on Programming Languages and Systems, 11(4):650– 665, 1989.

[26] Lasse R. Nielsen. A denotational investigation of defunctionalization. Technical Report BRICS RS-00-47, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2000.

[27] John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363–397, 1998. Reprinted from the proceedings of the 25th ACM National Conference (1972), with a foreword.

[28] Christopher Strachey and Christopher P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Higher-Order and Symbolic Computation, 13(1/2):135–152, 2000. Reprint of the technical monograph PRG-11, Oxford University Computing Laboratory (1974), with a foreword.

[29] Mitchell Wand. Semantics-directed machine architecture. In Richard De-Millo, editor, Proceedings of the Ninth Annual ACM Symposium on Principles of Programming Languages, pages 234–241. ACM Press, January 1982.

Recent BRICS Report Series Publications

RS-04-5 Biernacki Dariusz and Danvy Olivier. From Interpreter to Logic Engine by Defunctionalization. March 2004. 20 pp. To appear in Bruynooghe, editor, International Symposium on Logic Based Program Development and Transformation, LOPSTR ’03 Proceedings, Revised Selected Papers, LNCS, 2003. This report supersedes the earlier BRICS report RS-03-25.

RS-04-4 Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal Strategies in Priced Timed Game Automata. February 2004. 32 pp.

RS-04-3 Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines. February 2004. 17 pp. This report supersedes the earlier BRICS report RS-03-24. Extended version of an article to appear in Information Processing Letters.

RS-04-2 Gerth Stølting Brodal, Rolf Fagerberg, Ulrich Meyer, and Norbert Zeh. Cache-Oblivious Data Structures and Algorithms for Undirected Breadth-First Search and Shortest Paths. February 2004. 19 pp.

RS-04-1 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy’s Merge. January 2004. 16 pp.

RS-03-53 Kyung-Goo Doh and Peter D. Mosses. Composing Programming Languages by Combining Action-Semantics Modules. December 2003. 39 pp. Appears in Science of Computer Programming, 47(1):2–36, 2003.

RS-03-52 Peter D. Mosses. Pragmatics of Modular SOS. December 2003. 22 pp. Invited paper, published in Kirchner and Ringeissen, editors, Algebraic Methodology and Software Technology: 9th International Conference, AMAST ’02 Proceedings, LNCS 2422, 2002, pages 21–40.

RS-03-51 Ulrich Kohlenbach and Branimir Lambov. Bounds on Iterations of Asymptotically Quasi-Nonexpansive Mappings. December 2003. 24 pp.

RS-03-50 Branimir Lambov. A Two-Layer Approach to the Computability and Complexity of Real Numbers. December 2003. 16 pp.