日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

Prolog 再考: 急がないで推測
オレッグ・キセリョーヴ

亀山 幸義 .

古典 Prolog は、項代数、非決定性、単一化, 反例探索、論理と制御の分離という最も基本的な概念を簡潔にまとめている素敵な言語である。プログラムが双方向に動くのは不思議だ。しかし、現実の Prolog プログラムが持つ問題カットの多用、算術, FFI, committed choice, 頻繁な発散など-が古典 Prolog の利点を打消してしまう。
古典 Prolog は、魅力的な問題だ。古典 Prolog の勉強をして、その問題から教訓を学ぶ必要がある。その教訓として、非決定性は基本的だが、標準の実行モードになるべきではない、そして、遅延推測を使わないと性能が悪すぎる、ということがあげられる。
古典 Prolog の利点は、普通の正格な関数型言語で実装できる。本研究では、遅延推測を OCaml ライブラリとして実現し、そのライブラリを使って Prolog の典型的な例を記述する。加えて、双方向に動く型推論、committed
choice (maximal munch) を使って双方向に動く parser combinators を記述する。これらは古典 Prolog で実装できない。これらの実装から、論理変数の独特な性質、エルブラン領域の列挙の最適化の立場から見た単一化、WAM
へのコンパイルなどが理解できる。

mance requires the extensive use of problematic

1 Introduction

features such as cut.

Classical Prolog [1, 2] – the archetype and themised when interfacing with mainstream language

eponym of logic programming – is a fascinating lan-

libraries, which are deterministic and cannot run

guage, especially for natural language processing

backwards. Divergence is the constant threat, forc-[3, 4] and knowledge representation, planning anding the Prolog programmers to forsake the declara-reasoning [5, 6]. It is greatly appealing to declar-

tive specification and program directly against theatively state the properties of a problem and let

search strategy. All in all, Classical Prolog is thethe system find the solution. Most intriguing is theexquisite square peg in the world with mostly roundability to run programs ‘forwards’ and ‘backwards’.

holes.

We recall these irresistible features in §2. 1.

Purity is also compro-

The case in point is the ubiquitous committed

The concise and declarative formulation of prob-

choice [8], which is necessary to express the per-lems is the gift of non-determinism and the rea-vasive ‘maximal munch’ parsing convention (§5) as

son for its invention [7]. Classical Prolog makes

well as the ‘don’t care non-determinism’. For these

non-determinism the default computational mode.

reasons, committed choice is natively supported in

Taken to such extreme, non-determinism turns

Prolog, as the ‘soft-cut’. However, Prolog programsfrom virtue into vice. Quite many computations

with committed choice can no longer be run back-and models are mostly deterministic. Implement-

wards: see §5. 1.

ing them in Prolog with any acceptable perforRethinking Prolog
Oleg Kiselyov, Yukiyoshi Kameyama, Tsukuba.

The history of Prolog [2], designed on the foundation of non-determinism and resolution, is adapting, restricting or overcoming these ideas to makethe language general-purpose. An alternative is toand bringing them into the conventional functional-

start with a mature general-purpose, determinis-

programming language. Such bottom-up approachtic programming language, with a proven record

is not only practical but also theoretically reveal-of solving real-world problems – and add non-ing. We see in §6 how logic variables and unifica-

determinism. Is this a good alternative? We ex-tion naturally emerge as a “mere optimization” ofplore this question in §3.

non-deterministic search.

We use Hansei – aprobabilistic programming system implemented asa library in OCaml [9, 10] – to solve a number

2 Fascination and Disappointment ofClassical Prologof classic logic programming problems, from ze-

In this section we recall how Classical Prolog

bra to scheduling, to parser combinators, to re-continues to hold our fascination. We also recall

versible type checking. The complete code accom-

the disappointments and eventual realization thatpanying the is available at http://okmij.org/ftp/

Classical Prolog is in reality not a general-purpose

kakuritu/logic-programming.html.

programming language. This realization drives us

Many mature functional languages easily let nondeterminism in, thanks to the features like Mon-to introduce the best Prolog features in the general
purpose, functional languages, in §3.

adPlus in Haskell or delimited control libraries
in Scala, OCaml or Scheme.

Alas, the cheaply

added non-determinism has a ridiculously poor performance even on toy problems.

Making non-determinism usable requires non-trivial insight:
lazy sharing, see §3. 2.
As a larger case study, §5. 2 presents a parser

2. 1 The Append example
All the best features of Prolog can be illustrated
in only two lines of code: the append relation:
append([], L,L).
append([H|T],L,[ H|R]) :− append(T,L,R).

combinator library to build maximal-munch parsers

The three-place predicate append establishes the re-that are reversible: a parser may run forwards tolation between three lists l1, l2 and l3 such thatparse a given string, and backwards to generate

l1 is a prefix and l2 is the corresponding suﬃx of

all parseable strings, the language of its grammar.

l3. The two lines declare that the empty list is a

Such reversible parser combinators with the max-

prefix of any list, a list is a suﬃx of itself, and aimal munch cannot be idiomatically implemented

list prefix is the sequence of its initial elements.

in Classical Prolog.

When we ask a Prolog system if there is a list

Our argument is the argument for functional

X such that append([t,t,t],[f,f],X) holds, Prolog an-

logic programming [11] – however, realized not as aswers ‘Yes’. Furthermore, it gives us that list X – asstandalone language such as Curry but as a library

if append were a function to concatenate two lists.

in the ordinary programming language. We stress?− append([t,t, t],[ f , f ], X).

that we do not advocate the embedding of Prolog

X = [t, t, t, f , f ].

in a general-purpose language. Many such embeddings have been done (in Scheme, Haskell, Scala,etc), all sharing the drawbacks of Classical Prolog.
Rather, we advocate transcending Prolog: taking
its best features – separation of the model specification from the search and non-determinism –Prolog’s append is however is not just a function: it is a relation. We may specify any two lists
and query for the other one that makes the relation
hold. For example, let us check if a given list has
a given prefix, and if so, remove it (that is, obtainthe corresponding suﬃx).
?− append([t,t], X,[ t, t, t, f , f ]).
X = [t, f , f ].

2. 2 Disappointments
The append relation is the best illustration of
Prolog – of its fascination, and, as we see in thissection, of some of its disappointments. Recall our

Likewise, we can check for, and remove, a given
suﬃx. If the list concatenation was like running

example of finding all lists R with the given prefix[t,t,t].

append forwards, prefix removal is like running it?− append([t,t, t], X,R).

backwards.

R = [t, t, t| X].

There are more ways to run append; for example:
find all lists R with the given prefix [t,t,t] and an

The given answer compactly represents the infinite

arbitrary suﬃx X.

set of lists. Only some of them are boolean lists,?− append([t,t, t], X,R).

that is, made of elements t and f. We cannot en-

R = [t, t, t| X].

force the type of the list elements through a static
type system: Classical Prolog is untyped. One may

The answer is given on one line, which, however,compactly represents an infinite number of solu-

think the lack of a type system is a minor drawback.
The easy-to-write specification for boolean lists:tions. Hence a question in Prolog may have morethan one answer. We get the first hint of non-bool(t). bool(f ).

determinism.

boollist ([]).

If we ask for all lists with the [f,f] suﬃx, Pro-

boollist ([ H|T]) :− bool(H), boollist (T).

log lists the solutions, as an infinite stream. Non-lets us declare that the lists R and X in the original

determinism becomes clear.

example are in fact boolean:?− append( ,[f, f ], R).

?− append([t,t, t], X,R), boollist (X), boollist (R).

R = [f, f ] ;X = [],R = [t, t, t] ;R = [ G328, f, f ] ;X = [t],R = [t, t, t, t] ;R = [ G328, G334, f, f ] ;X = [t, t],

R = [t, t, t, t, t] ;R = [ G328, G334, G340, f, f ].

X = [t, t, t], R = [t, t, t, t, t, t] ;

...

...

Append can also split a given list in all possible

The result is disappointing.

First, boolean lists

ways, returning its prefixes and suﬃxes. If the list

with the given prefix are no longer compactly rep-

is finite, we obtain the finite number of answers.

resented. More worrisome, Prolog is stuck on t. For?− append(X,Y,[t,t, t, f , f ]).
X = [],

Y = [t, t, t, f , f ] ;example, [t,t,t,f] is also a boolean list with the prefix[t,t,t], but we do not see it among the answers. The

X = [t], Y = [t, t, f , f ] ;built-in search strategy of Prolog is incomplete. If

X = [t, t], Y = [t, f , f ] ;we change the order of the predicates in the con-

X = [t, t, t], Y = [f, f ] ;junction

X = [t, t, t, f ], Y = [f] ;?− boollist (X), boollist (R), append([t, t, t], X,R).

X = [t, t, t, f , f ], Y = [] ;false . % no more answers

we find to our dismay that Prolog loops after giving the first solution. Therefore, Classical Prolog

programs are not as declarative as one may think:the order of predicates and clauses matters a greatdeal. One must be very familiar with the evaluation strategy to write programs that produce any
result, let alone produce the result fast.
There are more problems, such as numericalcalculations or interfacing with foreign functions.
They can be dealt with various success in modern
Prolog systems, via mode inference and constraintsolving systems – which take us beyond Classical

Basic functions
type prob = float
val dist: (prob ∗ α) list → αval fail: unit → αval reify0 : (unit → α) → α pV
val letlazy : (unit → α) → (unit → α)Convenient derived functions
val flip
val uniformly...
val exact reify
val reify part

Prolog.
The biggest problem is non-determinism as thedefault. Many real-life problems are mostly deter-: prob → bool
: α array → α: (unit → α) → α pV
: int option → (unit → α) →(prob ∗ α) list...
図1

Hansei interface

ministic, or involve long segments of deterministic computations (e.g., number crunching). Encod-

such as flip, flipping a coin, and the uniform selec-

ing such problems eﬃciently in Prolog is very dif-tion; exact reify exhaustively searches through all

ficult, often requiring ‘cut’ and other impure fea-

the choices and produces the flattened choice tree,tures, which destroy the reversibility and do notor the probability table.

play well with constraint solving. §4 gives one ex-

Hansei (and similar libraries for Scala or Haskell)

ample, of the need for restricting non-determinism

show that just adding non-determinism to an es-

and the problem it causes for Prolog.

tablished language is straightforward. With little

When a problem suits Prolog, the answer is

eﬀort we can already write Prolog-like programs,

breathtakingly elegant. But most of the time it

and we do in §3. 1. We also see that the cheap non-is not.

determinism is cheap indeed: it performs poorly

3 An alternative to Prolog

and is prone to divergence. §3. 2 presents a smart

As an alternative to Classical Prolog we add non-alternative. Our running example is writing thedeterminism to an ordinary language, where deter-classic append relation of Prolog in Hansei.

minism is default. An example is a library called
Hansei†1 , which adds weighted non-determinism

3. 1 Cheap non-determinism(probabilities) to the ordinary OCaml. (We will

At first blush, there is little to do. OCaml al-

ignore the probabilities in this paper.)ready has a built-in operation @ to concatenate

The primitives of the library, see Figure 1, are

two lists. Extending this function to a relation isdist, to non-deterministically choose an element

also straightforward, thanks to non-determinism.

from a list, and fail. There is also a strange sound-

We demonstrate on the example of running append

ing function reify0 that turns a program into abackwards: un-concatenating a given list and pro-tree of choices αpV, letting us program our own

ducing all its possible prefixes and the correspond-search strategies.

ing suﬃxes. The task thus is to represent the fol-

The library has many conve-

nient functions written in terms of the primitives,†1 http://okmij.org/ftp/kakuritu/

lowing Prolog code in OCaml?− append(X,Y,[t,t, t, f , f ]).

The key idea is that running backwards is tanta-(0.0002, ([ true; true; true], [ false ; false ]));

mount to generate-and-test: in our case, generat-(0.0002, ([ true; true; true; false ], [ false ]));

ing candidate prefixes and suﬃxes and then testing(0.0002, ([ true; true; true; false ; false ], []))]

if they make up the given list. We merely need agenerator of lists, all boolean lists in our example.

It really works as intended, although it takes about
2 seconds even for such a trivial example. Alas, if

let rec a list() =we increase the search bound (the first argument

if flip 0.5 then []else flip 0.5 :: a listof reify part) to 35, the program diverges. It is not()

diﬃcult to see why: a list really generates all pos-

Declaratively, a boolean list is either [] or a boolean

sible boolean lists; only very few of them add up

list with either true or false at the head. In Han-

to t3f2; the others will have to be rejected. The

sei terms, the thunk a list is a probabilistic model,

problem with cheap non-determinism is generating

which we then have to run. Running the model de-vastly too many candidate solutions, almost all of

termines the set of possible worlds consistent withwhich are rejected.

the probabilistic model: the “model” of the model.
The set of outputs in these worlds is the set of an-

3. 2 Smart non-determinism

swers. Hansei oﬀers a number of ways to run mod-To use non-determinism eﬀectively requires so-

els and obtain the answers and their weights. We

phistication: to avoid generating and considering

will be using iterative deepening, reify part, a ver-clearly failing solutions. The key idea is laziness –sion of exact reify whose first argument is the depth

delaying the choices till the last possible moment.

search bound (infinite, if None). For example, we

Looking back at Prolog gives us a hint. OCaml

test a list by generating a few sample boolean lists:

lists are fully determined: [true; false] is the list of
the definite size with definite elements. Prolog lets

reify part(Some 3) a list

⇝ [(0.5, []);

(0.125, [ false ]); (0.125, [ true])]

us write partly determined lists, such as [t|X]; weknow the head of the list but do not yet know what

Everything is set to implement our idea of run-follows. Comparing this list with others, such as

ning @ backwards, to unconcatenate the sample list[t,f|Y], increases our knowledge. Some other com-

t3f2 obtaining all its prefixes and the corresponding

parisons, e.g., with [f|Z], clearly fail; they fail re-

suﬃxes.

gardless of what X or Z really are, so we do not

let t3f2 = [true; true; true; false ; false ]reify part(Some 25) (fun() →let x = a list () inlet y = a list () ineven have to generate them.
To follow the Prolog’s hint, we define party determined lists in OCaml: boolean lists with a nondeterministic spine.

let r = x @ y intype bl = Nil | Cons of bool ∗ blist

if not (r = t3f2) then fail ();and blist = unit → bl(x, y))

We introduce nil and cons as easy-to-use construc-⇝[(0.0002, ([],

tors of lists and a function to convert blists into
[ true; true; true; false ; false ]));

(0.0002, ([ true], [ true; true; false ; false ]));
(0.0002, ([ true; true], [ true; false ; false ]));

ordinary OCaml lists to show them. Sample lists
t3 and f2 will be used in the examples.

let nilblush looks like the identity function. It is another: blist = fun () → Nil

let cons : bool → blist → blist =primitive of Hansei, taking a thunk and returning a

fun h t () → Cons (h,t)

thunk. When we force the resulting thunk, we force

val list of blist

the original one, and remember the result. All fur-: blist → bool list

ther forcing return the same result. In functional
let t3 = cons true (cons true (cons true nil ))logic programming, this is called “call-time choice”.

let f2 = cons false (cons false nil )In quantum mechanics, it is called “wave-function
collapse”. Before we observe a system, for example,

The append is defined as an ordinary recursivefunction, which pattern-matches on the list.

a still spinning coin, there could indeed be several
choices for the result. After we observed the sys-

let rec append l1 l2 =

tem, all further observations give the same result.

match l1 () with

Like the quantum-mechanical entanglement, letlazy| Nilis a way to share the non-deterministic state.

→ l2| Cons (h,t) → cons h (fun () → append t l2 ())

reify part

Here is an example of its use:
reify part(Some 3) (fun() →let x = a blist () inNone (fun () →list of blist

Passing a blist as the second argument of append,

list of blist(append t3 f2))

⇝ [(1., [ true; true; true; false ; false ])](append t3 x))⇝[(0.5, [ true; true; true]);giving the expected result. We have defined append(0.125, [ true; true; true; false ]);as a function, and can indeed run it as the concate-(0.125, [ true; true; true; true])]nation function, ‘forwards’.
Prolog also lets us concatenate lists that are partially or wholly unknown, represented by logic variables. For example, append([t,t,t],X,R) will enumerate all lists with [t,t,t] as the prefix, see §2. 1. If weare interested in only boolean lists, we had to com-lets us see, within the given search bound, allboolean lists whose first three elements are true.
Unlike the Prolog code, we are no longer stuck generating lists whose all elements are true.
The moment of truth is running append backwards. We have already explained the key idea ofplicate the Prolog code

generate-and-test in §3. 1. The code in that section

append([t, t, t], X,R), boollist (X), boollist (R).
and faced the problem of incomplete search: Prolog

is trivial to adapt to partially determined lists blist;
we only need the comparison function on blists:

could not produce any lists that included f. In Han-

let rec bl compare l1 l2 =sei, the role of logic variable as the representation

match (l1 (), l2 ()) withfor some boolean list is played by a generator:| (Nil , Nil ) → true

let rec a blist| (Cons (h1,t1), Cons (h2,t2)) →() : blist =h1 = h2 && bl compare t1 t2

letlazy (fun () →|uniformly [| Nil ;Cons(flip 0.5, a blist()) |])

We need the magical function letlazy, which at first→ falseApplying the generate-and-test idea to reverse theappend:None (fun() →ferent choices. Ordinary lazy evaluation is imple-

let l = append t3 f2 inmented by mutation of the ordinary, or global, or

let x = a blist () inshared memory – shared across all possible worlds.

let y = a blist () in

Non-deterministic laziness needs world-local mem-

let r = append x y inory [12].

reify part

if not (bl compare r l ) then fail ();(list of blist

x, list of blist

4 Parsing with committed choicey)gives the same, expected result as in §3. 1, but witha surprise. First, the result is produced 1000 times
faster. Second, the program terminates with the
expected six answers even though we imposed nosearch bound: the first argument of reify part isNone. Although x and y in the code will generate any boolean list, thanks to laziness, the search
space is eﬀectively finite, and quite small. Thus thereal speed-up due to laziness is infinite.

pressions and is commonly used in EBNF and othergrammar formalisms. Just as common is the socalled “maximal munch” restriction on the Kleenestar, forcing the longest possible match. After reminding why maximal munch is so prevalent, we
describe the grave problem it poses for parsers thatare meant to be run both forwards and backwards– that is, to parse a given stream according to thegrammar and to generate all parseable streams, theThe letlazy operation in the definition of a blist is
crucial:let rec a blist

Kleene star is an intrinsic operator in regular ex-

grammar’s language.
Maximal munch cuts shorter-match choices and() =reduces non-determinism – hence making forward

letlazy (fun () →runs faster. On the downside, when running theuniformly [| Nil ;parser backwards the cut choices mean lost solu()) |])tions and the (greatly) incomplete language gener-

The operation uniformly guesses at the top con-ation. Hansei removes the downside. Parsers built

structor of the list: Nil or Cons; letlazy delays thewith the Hansei parser combinator library support

guess, letting the program proceed until the result

maximal munch and can be run eﬀectively back-of the guess is truly needed. Hopefully the pro-wards to generate the complete language, without

gram rarely gets to that point because the searchomissions.

encountered a contradiction at some other place.

necessary features, in particular, the nested infer-Cons(flip 0.5, a blist

Laziness in non-deterministic computations ishence indispensable.

Non-deterministic laziness

Surprisingly, Hansei already had theence.

5 Maximal munch rule

however is diﬀerent from the familiar facility to de-

The maximal munch convention is so common inlay the computation and memoize its result, suchparsing that it is hardly ever mentioned. For ex-

as OCaml’s lazy, Scheme’s delay or Haskell’s lazyample, a programming language specification cliche

evaluation. We may think of a non-deterministic

defines the syntax of an identifier as a letter fol-choice, flipping a coin, as splitting the current

lowed by a sequence of letters and digits, or, in theworld. In one world, the coin came up ‘head’, in

extended BNF,

the other it came ‘tail’. If we are to cache the result, we should use diﬀerent memo tables for different worlds, because diﬀerent worlds have dif-

identifier:: = letter letter or digit ∗where∗,the Kleene star,denotes zero or

more repetitions of letter or digit.

munch, it looks as follows:

In the string

many0(P,S,S).

”var1 + var2” we commonly take var1 and var2

many0(P,S,Rest) :− call (P,S,Srem), many0(P,Srem,Rest).

to be identifiers. However, according to the above
where P is an arbitrary parser. Thus many0(charA,S,R)grammar every prefix of an identifier is also an iden-

will recognize or generate the prefix of S with zerotifier. Therefore, we should regard v, va and var as

or more ’a’ characters.

identifiers as well. To avoid such conclusions andstandard Prolog predicate to call a goal indirectly:

the need to complicate the grammar, the maximalcall(charA,S,R) is equivalent to the charA(S,R).)

munch rule is assumed: letter or digit∗ denotes theThanks to the first clause, many0(P,S,R) always

longest sequence of letters and digits. Without therecognizes the empty string. Here is how we recog-

maximal munch, we would have to write
identifier:: = letter letter or digit(Recall that call is thenize a∗ in the sample input stream [a,a,b]:∗[ look−ahead: not letter or digit]?− many0(charA,[a,a,b],R).
R = [a, a, b] ;It is not only awkward, requiring the notation forlook-ahead, but also much less eﬃcient. If ∗ means
mere zero or more occurrences, letter or digit∗ on
input ”var1 ” will match the empty string, ”a”,

R = [a, b] ;R = [b]and generate the language of a∗ :”ar” and ”ar1”. Only the last match leads to the?− many0(charA,S,[]).

successful parse of the identifier, recognizing var1.

S = [] ;Maximal munch cuts the irrelevant choices. It has

S = [a] ;proved so useful that it is rarely explicitly stated

S = [a, a] ;when describing grammars.

S = [a, a, a] ; ...
To implement the maximal munch, many should

5. 1 Maximal munch in Prolog:Re-versibility lost
Maximal munch however destroys the reversible
parsing, the ability to run the parser forward (as aparser or recognizer) and backward (as a language
generator). We illustrate the problem in Prolog.
A recognizer in Prolog is a relation between two
streams (lists of characters) S and Srem such thatcall the argument parser as long as it succeeds. To
tell if the parser fails or succeeds we turn to softcut. Recall, soft-cut P ∗→Q; R is equivalent to the
conjunction P, Q if P succeeds at least once. Softcut commits to that choice and totally discards R inthat case. R is evaluated only when P fails from theoutset. Soft-cut lets us write many with maximal
munch:

Srem is the suﬃx of S. In a functional language, wewould say that a recognizer recognizes the prefix in
S, returning the remaining stream as Srem. Here is
the recognizer for the character ’a’:charA([a| Srem],Srem).
The Kleene-star combinator (typically called

many(P,S,Rest) :−call (P,S,Srem) ∗→ many(P,Srem,Rest) ; S = Rest.
Now the the empty string is recognized (i.e.,
S = Rest) only if the parser P fails. Recognizinga∗ in the sample inputmany) takes as an argument a recognizer and re-?− many(charA,[a,a,b],R).

peats it zero or more times. Without the maximal

R = [b].

becomes quite more eﬃcient. There is only one
choice, for the longest sequence of as. However,attempting to generate the language a∗ :A parser takes a stream and returns the parsing result,
the result of a semantic action, and the remainder ofthe stream:type stream v = Eof | Cons of char ∗ stream
and stream = unit → stream v
type α parser = stream → α ∗ stream?− many(charA,S,[]).
<loops>Primitive parser

leads to an infinite loop. The argument recognizer,
charA, when asked to generate, always succeeds.

val let p char : char → char parser

Therefore, the recursion in many never terminates.

checks the current element of the stream is the given
character, returning it.

When running backwards, the recognizer tries to

Parsing combinators

generate the longest string of as – the infinite string.
Although the empty string belongs to the languagea∗ , we fail to generate it.

5. 2 Maximal munch in Hansei:

Re-

versibility regained
The Hansei parser combinator library, Figure 3,
supports many, which, unlike the one in Prolog, noval (<∗> ) : (α → β) parser → α parser → β parserval ( <∗ ) : α parser → β parser → α parser
let (<|> ) : αparser → α parser → α parser =fun p1 p2 st → uniformly [| p1;p2| ] stcombine parsers and their semantic actions and express
the rules of the grammar: (<∗> ) combines parsers sequentially and (<|> ) expresses the alternation. The
combinator ( <∗ ) is the specializations of (<∗> ).
図3

Hansei parser combinator librarylonger forces the trade-oﬀ between eﬃcient parsing and generation. Hansei’s many obeys maximal
munch and generates the complete language, withno omissions. Hansei lets us have it both ways. Before describing the implementation, we show a few| C of (unit → α pV)
and α pV = (prob ∗ α vc) list
val reify0 : (unit → α) → α pV
val reflect

representative examples, Figure 2.
Examples 5-7 show the argument parsers with

: α pV → α

The primitive reify0 converts a probabilistic com-choices, even overlapping choices as in Example 7.

putation to a lazy tree of choices αpV, whose nodes

The combinator many (actually, many1 defined as

contain found solutions V x or not-yet-exploredmany1 p = p <∗ many p) may nest. In Example 3,

branches.

a∗a does not recognize ”aaa” since the a∗ munches

reify0, turns a tree of choices into a probabilistic

the entire stream leaving nothing for the parser ofprogram that will make those choices. The prim-

the final a. This is the expected behavior underitive reify0 is fundamental in Hansei: probabilistic

maximal munch. Example 7 shows no parse for theinference is implemented by first reifying a program

same reason. Finally in the last example we gen-(the generative model) to the tree of choices and∗

The primitive reflect, the inverse oferate the complete language for a , including thethen exploring the tree in various ways. For in-empty string.

stance, the full tree traversal corresponds to exact

To implement the maximal munch in Hansei weinference.

need something like soft-cut, the ability to detect

Soft-cut can also be implemented as a choice-a failure and proceed. Hansei has exactly the righttree traversal, first success below, which explores

tools: reify0 and reflect:

the branches looking for the first V leaf. It returns

type α vc = V of α

the tree resulting from the exploration, which couldParserStreamResult1

many (p char ’a’)

”aaaa”

unique2

many (p char ’a’) <∗> p char ’b’”b”

unique3

many (p char ’a’) <∗ p char ’a’”aaa”

no parse

4

many (p char ’a’) <∗> many (p char ’a’))”aaa”

unique5

many ((p char ’a’) <|> (p char ’b’))”ababb”

unique6

many ((many1 (p char ’a’)) <|>”aaabab”

unique<∗ p char ’a’”aaa”

no parse

many (p char ’a’)random””, ”a”, ”aa”, . . .

(p char ’b’)))(many17

8

many ((p char ’a’ <∗ p char ’a’) <|> p char ’a’)

図2

Examples of maximal munch parsing

be empty if no V leaf was ever found. Soft-cut thentions. They take a stream, attempt to recognize

is simply

its prefix and return the rest of the stream on suc-val first success: α pV → α pV

cess. They cannot be run backwards. However,we achieve the same result – producing the set ofparseable streams – by generating all streams, feed-

let soft cut :(unit → α) → (α → ω) → (unit → ω) → ω =ing them to the parser and returning the streams

fun p q r →that parsed completely. Since the number of possi-

match first success (reify0 p) withble streams is generally infinite, we have to generate| [] → r ()them lazily, on demand. To ensure completeness –| t→ q (reflect

to avoid losing any solutions – the parsers shouldt)have the property
We write many in terms of the soft-cut as we did inmany p (s1 ⊕ s2) = many p s1 ⊕ many p s2

Prolog:let many : α parser → α list

parser = fun p →where ⊕ stands for non-deterministic choice. Surprisingly, many p already satisfies it.

let rec self st =The trickis laziness in the stream and Hansei’s support ofsoft cut(* check if p succeeded *)in probabilistic programs – in other words, a prob-(fun () → p st )abilistic model may itself perform inference, over(* continue with p *)an inner model. In order for this to work correctly,(fun (v, st ) →let (vs, st ) = self st in

we had to ensure that
let x = letlazy (s1 ⊕ s2) in(v:: vs, st ))(fun () → ([], st ))nested inference. The primitive reify0 may appear

reify0 (fun () → model x)(* if p failed *)in self≡

The second question is avoiding losing solutions

let x = letlazy s1 in reify0 (fun () → model x) ⊕when running the parser “backwards”. Unlike Pro-

let x = letlazy s2 in reify0 (fun () → model x)log, Hansei parsers are functions rather than rela-

where x is demanded in model.

That is, reify0

should reify only the choices made by the innergetting stuck in one infinite sub-region. Hansei,

program, and let the outer choices take eﬀect. The

among other similar systems, satisfies all these re-stream generator has to be lazy, so it has the form

quirements.

letlazy (s1 ⊕ s2). Comparing the nested inference

Logic variables and unification have been intro-

property with the code for many reveals that the

duced by Robinson as a way to ‘lift’ ground reso-

key property of many p (s1 ⊕ s2) is satisfied with-lution proofs of Herbrand, to avoid generating theout us needing to do anything. Our many has ex-vast number of ground terms [13]. Logic variables

actly the right semantics.

eﬀectively delay the generation of ground terms to
the last possible moment and to the least extent.

6 Conclusions

Doing computations only as far as needed is also theClassical logic programming all too often forces

goal of lazy evaluation. It appears that lazy eval-

us to choose between eﬃciency and expressiveness,uation can make up for logic variables, rendering

on one hand, and completeness on the other hand.

Herbrand’s original approach practical. It remains

Negation and committed choice make logic pro-a fascinating task to be able to systematically de-grams easier to write and, in some modes, fasterrive a unification procedure.

to run. Alas, some other modes (informally, running ‘backwards’) become unusable or impossible.

参考文献

Kleene star is a good example of the trade-oﬀ:[ 1 ] William F. Clocksin and Christopher S. Mel-maximal munch simplifies the grammar and makes

lish. Programming in Prolog. Springer, 5 edi-

parsing eﬃcient, but destroys the ability to gen-tion, 2003.

erate grammar’s language. Functional logic pro-[ 2 ] Peter Van Roy. 1983-1993: The wonder years

gramming systems can remove the trade-oﬀ. Prop-of sequential prolog implementation. Techni-

erly implemented encapsulated search (nested in-cal Report 36, Paris DEC Research Labora-

ference, in Hansei) lets us distinguish the choices oftory, December 1993.

the parser from the choices of the stream and cut[ 3 ] Fernando C. N. Pereira and Stuart N. Shieber.

only the former. Perhaps surprisingly this distinc-

Prolog and Natural-Language Analysis. Centertion just falls out of the need for non-deterministic

for the Study of Language and Information,

stream to be lazy. Thus Kleene star with maximal munch lets us parse and generate the complete
language. In Hansei, we can have it both ways.
We have gone back to Herbrand: we build theHerbrand universe (the set of all ground terms) andStanford, California, 1987.
[ 4 ] Patrick Blackburn, Johan Bos, and Kristina
Stiegnitz. Learn Prolog Now! College Publications, London, 2006.
[ 5 ] T. Moto-oka, editor. Fifth Generation Com-

explore it to find a model of a program. We build

puter Systems.

the universe by modeling ‘logic variables’ as gener-

1982.

North-Holland, New York,ators for their domains. Since the Herbrand uni-

[ 6 ] Committee for Development and Promotion

verse for most logic programs is infinite, non-strictof Basic Computer Technology. Fifth genera-

evaluation is the necessity. Furthermore, since logic

tion computer systems project final evaluation

variables may occur several times, we must be able
to correlate the generators. Finally, we need a systematic way of exploring the search space, without

report. ICOT Journal, No. 40, pp. 3–24, 1994.
[ 7 ] Michael O. Rabin and Dana Scott.

Finiteautomata and their decision problems. IBM

Journal of Research and Development, Vol. 3,
pp. 114–125, 1959.

June 2009. AUAI Press.
[11] Michael Hanus.

Multi-paradigm declara-

Pruning in logic programming.

tive languages. In Proceedings of the Inter-

Technical Report 95/16, Department of Com-national Conference on Logic Programming

puter Science, University of Melbourne, Mel-(ICLP 2007), No. 4670 in LNCS, pp. 45–75.

bourne, Australia, June 1995.

Springer, 2007.

[ 8 ] Lee Naish.

[ 9 ] Oleg Kiselyov and Chung-chieh Shan. Embed-[12] Sebastian Fischer, Oleg Kiselyov, and Chung-ded probabilistic programming. In Walid Mo-

chieh Shan. Purely functional lazy nondeter-

Proceedings of theministic programming. Journal of Functional

Working Conference on Domain-Specific Lan-

Programming, Vol. 21, No. 4–5, pp. 413–465,

guages, No. 5658 in LNCS, pp. 360–384.

2011.

hamed Taha,

editor,Springer, 15–17 July 2009.

[13] John Alan Robinson.

Computational logic:[10] Oleg Kiselyov and Chung-chieh Shan. Mono-

Memories of the past and challenges for the fu-

lingual probabilistic programming using gen-ture. In Proceedings of the First International

eralized coroutines. In Proceedings of the 25th

Conference on Computational Logic, No. 1861

Conference on Uncertainty in Artificial Intel-

in LNAI, pp. 1–24, 2000.

ligence, pp. 285–292, Corvallis, Oregon, 19–21