1: %Final version of system description paper for CADE 21 (2007).
2:
3: \documentclass{llncs}
4: \usepackage{proof}
5: \newcommand{\defeq}{\mathrel{\stackrel{{\scriptstyle\triangle}}{=}}}
6: \newcommand{\Dscr}{{\cal D}}
7: \newcommand{\false}{\hbox{\sl false}}
8:
9:
10: \begin{document}
11: \title{The Bedwyr system for model checking over syntactic expressions}
12: \author{
13: David Baelde\inst{1} \and
14: Andrew Gacek\inst{2} \and
15: Dale Miller\inst{1} \and
16: Gopalan Nadathur\inst{2} \and \\
17: Alwen Tiu\inst{3}
18: }
19: \institute{
20: INRIA \& LIX, \'Ecole Polytechnique \and
21: Digital Technology Center and Dept of CS, University of Minnesota\and
22: Australian National University and NICTA
23: }
24: \maketitle
25:
26: \section{Overview}
27:
28: Bedwyr is a generalization of logic programming that allows model
29: checking directly on syntactic expressions possibly containing
30: bindings. This system, written in OCaml, is a direct implementation of
31: two recent advances in the theory of proof search. The first is
32: centered on the fact that both finite success and finite failure can
33: be captured in the sequent calculus by incorporating inference rules
34: for {\em definitions} that allow {\em fixed points} to be explored.
35: As a result, proof search in such a sequent calculus can capture
36: simple model checking problems as well as may and must behavior in
37: operational semantics. The second is that higher-order abstract
38: syntax is directly supported using term-level $\lambda$-binders and
39: the $\nabla$ quantifier. These features allow reasoning
40: directly on expressions
41: containing bound variables.
42:
43: \section{Foundations}
44:
45: The logical foundation of Bedwyr is the logic called LINC
46: \cite{tiu04phd}, an acronym for ``lambda, induction, nabla, and
47: co-induction'' that is an enumeration of its major components. LINC
48: extends intuitionistic logic in two directions.
49:
50: \paragraph{Fixed points via definitions.}
51: Clauses such as $A\defeq B$ are used to provide (mutually) recursive
52: definitions of atoms. Once a set $\Dscr$ of such definition clauses
53: has been fixed, LINC provides inference rules for introducing atomic
54: formulas based on the idea of unfolding definitions. Unfolding on the
55: right of the sequent arrow is specified by the following {\em
56: definition-right} rule:
57: \[
58: \vcenter{
59: \infer
60: {\Sigma:\Gamma\vdash A}
61: {\Sigma:\Gamma\vdash B\theta}}
62: \hbox{\ , provided $A'\defeq B\in\Dscr$ and $A'\theta=A$.}
63: \]
64: This rule resembles backchaining in more conventional logic
65: programming languages. The {\em definition-left} rule is a case analysis
66: justified by a closed-world reading of a definition.
67: \[
68: \infer{\Sigma:\Gamma, A \vdash G}
69: {\{\Sigma\theta:\Gamma\theta,B\theta\vdash G\theta
70: \ | \ A'\defeq B\in\Dscr\mbox{ and }
71: \theta \in csu(A, A')\}}
72: \]
73: Notice that this rule uses unification: the eigenvariables of
74: the sequent (stored in the signature $\Sigma$) are instantiated by
75: $\theta$, which is a member of a complete set of unifiers (csu) for
76: atoms $A$ and $A'$. Bedwyr implements a subset of this rule that is
77: restricted to {\em higher-order pattern unification} and, hence, to
78: a case where {\em csu} can be replaced by {\em mgu}. If an atom on
79: the left fails to unify with the head of any definition, the premise
80: set of this inference rule is empty and, hence, the sequent is proved:
81: thus, a unification {\em failure} is turned into a proof search {\em
82: success}.
83:
84: Notice that this use of definitions as fixed points implies that logic
85: specifications are not treated as part of a {\em theory} from which
86: conclusions are drawn. Instead, the proof system itself is
87: parametrized by the logic specification. In this way, definitions
88: remain fixed during proof search and the {\em closed world assumption}
89: can be applied to the logic specification. For earlier references to
90: this approach to fixed points see
91: \cite{girard92mail,schroeder-heister93lics,mcdowell97lics}.
92:
93:
94: \paragraph{Nabla quantification.}
95: Bedwyr supports the \emph{$\lambda$-tree syntax} \cite{miller00cl}
96: approach to higher-order abstract syntax \cite{pfenning88pldi}
97: by implementing a logic that provides
98: $(i)$ terms that may contain $\lambda$-bindings, $(ii)$ variables that
99: can range over such terms, and $(iii)$~equality (and unification) that
100: follows the rules of $\lambda$-conversion. Bedwyr shares these
101: attributes with systems such as $\lambda$Prolog. However, it
102: additionally includes the $\nabla$-quantifier that is needed to fully
103: exploit the closed-world aspects of LINC. This quantifier can be read
104: informally as ``for a new variable'' and is accommodated easily
105: within the sequent calculus with the introduction of a new kind of
106: local context scoped over formulas. We refer the reader to
107: \cite{miller05tocl} for more details. We point out here, however,
108: that $\nabla$ can always be given minimal scope by using the
109: equivalences $\nabla x.(A x * B x) \equiv (\nabla x. A
110: x) * (\nabla x. B x)$ where $*$ may be $\supset$, $\land$ or $\lor$ and
111: the fact that $\nabla$ is self-dual: $\nabla x.\lnot Bx
112: \equiv\lnot \nabla x. Bx$. When $\nabla$ is moved under $\forall$ and
113: $\exists$, it {\em raises} the type of the quantified variable: in
114: particular, in the equivalences
115: $\nabla x\forall y. F x y \equiv\forall h\nabla x. F x (h x)$ and
116: $\nabla x\exists y. F x y \equiv\exists h\nabla x. F x (h x)$,
117: the variable $y$ is replaced with a functional variable $h$. Finally,
118: when $\nabla$ is scoped over equations, the equivalence
119: $\nabla x(T x = S x) \equiv (\lambda x.T x)=(\lambda x.S x)$
120: allows it to be completely removed. As a result, no fundamentally new
121: ideas are needed to implement $\nabla$ in a framework where
122: $\lambda$-term equality is supported.
123:
124:
125: \section{Architecture}
126:
127: Bedwyr implements a fragment of LINC that is large enough to permit interesting
128: applications of fixed points and $\nabla$.
129: In this fragment, {\em all} the left rules are
130: invertible. Consequently, we can use a simple proof strategy
131: that alternates between left and right-rules, with the left-rules
132: taking precedence over the right rules.
133:
134:
135: {\em Two provers.} The fragment of LINC implemented in Bedwyr is given
136: by the following grammar:
137: \begin{eqnarray*}
138: L0 &::=&
139: \top\; |\; A\; |\; L0 \land L0\; |\; L0 \lor L0\; |\; \nabla x.~ L0\; |\; \exists x.~ L0 \\
140: L1 &::=&
141: \top\; |\; A\; |\; L1 \land L1\; |\; L1 \lor L1\; |\; \nabla x.~ L1\; |\; \exists x.~ L1\; |\;
142: \forall x.~ L1\; |\; L0 \supset L1 \\
143: \end{eqnarray*}
144: The formulas in this fragment are divided into {\em level-0} formulas,
145: given by $L0$ above, and {\em level-1} formulas, given by $L1$.
146: Implicit in the above grammar is the partition
147: of atoms into level-0 atoms and level-1 atoms. Restrictions apply to goal
148: formulas and definitions: goal formulas can be level-0
149: or level-1 formulas, and in a definition $A \defeq B$, $A$ and $B$ can
150: be level-0 or level-1 formulas, provided that the level of $A$
151: is greater than or equal to the level of $B$.
152:
153: Level-0 formulas are essentially a subset of
154: goal formulas in $\lambda$Prolog (with $\nabla$ replacing $\forall$).
155: Proof search for a defined atom of level-0 is thus
156: the same as in $\lambda$Prolog (and Bedwyr implements that fragment
157: following the basic ideas described in \cite{elliott91semi}).
158: We can think of a level-0 definition,
159: say, $p\,x \defeq B\,x$, as defining a set of elements $x$
160: satisfying $B\,x$. A successful proof search for $p\,t$ means
161: that $t$ is in the set characterized by $B$.
162: A level-1 statement like $\forall x. p\,x \supset R\,x$ would then
163: mean that $R$ holds for all elements of the set characterized by $p$.
164: That is, this statement captures the enumeration of a {\em model}
165: of $p$ and its verification can be seen as a form of model checking.
166: To reflect this operational reading of level-1 implications,
167: the proof search engine of Bedwyr uses two subprovers:
168: the Level-0 prover (a simplified $\lambda$Prolog engine),
169: and the Level-1 prover.
170: The latter is a usual depth-first goal-directed prover but with a
171: novel treatment of implication.
172: When the Level-1 prover reaches the implication $A\supset B$, it
173: calls the Level-0 prover on $A$ and gets in return a stream of answer
174: substitutions: the Level-1 prover then checks that, for every
175: substitution $\theta$ in that stream, $B\theta$ holds.
176: In particular, if Level-0 finitely fails with $A$, the implication is proved.
177:
178: As with most depth-first implementations of proof search, Bedwyr
179: suffers from some aspects of incompleteness: for example, the prover
180: can easily loop during a search although different choices of goal or
181: clause ordering can lead to a proof, and certain kinds of
182: unification problems should be delayed instead of attempted eagerly.
183: For a more detailed account on the incompleteness issues, we refer the
184: reader to \cite{tiu05eshol}.
185: Bedwyr does not currently implement static checking of types and the
186: stratification of definitions (which is required in the
187: cut-elimination proof for LINC). This allows us to experiment with a
188: wider range of examples than those allowed by LINC.
189:
190: {\em Higher-order pattern unification.} We adapt the treatment of
191: higher-order pattern unification due to Nadathur and
192: Linnell~\cite{nadathur05iclp}. This implementation uses the {\em
193: suspension calculus} representation of $\lambda$-terms. We avoid
194: explicit raising, which is expensive, by representing $\nabla$-bound
195: variables by indices and associating a {\em global} and a {\em local}
196: level annotation with other quantified variables.
197: The global level replaces raising over existential and universal
198: variables.
199: The local level replaces raising over $\nabla$-bound variables.
200: For example, the scoping in
201: $\forall{}x.\exists{}y.\nabla{}n.\forall{}z. F x y n z$
202: is represented by the following annotation:
203: $F x^{0,0} Y^{1,0} \#_0 z^{2,1}$
204: (we use lowercase letters for universal variables,
205: uppercase for existentials,
206: the index $\#_n$ for the $n$-th $\nabla$-bound variable,
207: and write in superscript the annotation $(global,local)$).
208: Using this annotation scheme, the scoping aspects of $\nabla$ quantifiers
209: are reflected into new conditions on local levels
210: but the overall structure of the higher-order pattern unification
211: problem and its mgu properties are preserved.
212:
213: {\em Tabling.} We introduced tabling in Bedwyr to cut-down exponential
214: blowups caused by redundant computations and to detect loops during
215: proof-search. The first optimization is critical for applications such
216: as weak bisimulation checking. The second one proves useful when exploring
217: reachability in a cyclic graph.
218:
219: Tabling is currently used in Bedwyr to experiment with proof search for
220: inductive and co-inductive predicates. A loop over an inductive predicate
221: that would otherwise cause a divergence can be categorized using
222: tabling as a failure.
223: Similarly, in the co-inductive case, loops yield success.
224: This interpretation of loops as failure or success is not part of the
225: meta-theory of LINC. Its soundness is currently conjectured, although
226: we do not see any inconsistency of this interpretation on the numerous
227: examples that we tried.
228:
229: Inductive proof-search with tabling is implemented effectively
230: in provers like XSB~\cite{sagonas06xsb} using, for example,
231: suspensions. The implementation of tables in Bedwyr
232: fits simply in the initial design of the prover but is much weaker.
233: We only table a goal
234: in Level-1 when it does not have free occurrences of variables
235: introduced by an existential quantifier; and
236: in Level-0 when it does not have any free variable occurrence.
237: Nevertheless, this implementation of tabling has proved useful
238: in several cases, ranging from graph examples to bisimulation.
239:
240: \newcommand{\step}[2]{\hbox{\sl step}~#1~#2}
241: \newcommand{\win }[1]{\hbox{\sl win} ~#1}
242: \newcommand{\simm}[2]{\hbox{\sl sim}~#1~#2}
243: \newcommand{\one }[3]{#1\stackrel{#2}{-\!\!-\!\!\!\to } #3}
244: \newcommand{\onep}[3]{#1\stackrel{#2}{-\!\!-\!\!\!\rightharpoonup} #3}
245:
246: \section{Examples}
247:
248: We give here a brief description of the range of applications of Bedwyr.
249: We refer the reader to {\tt\url{http://slimmer.gforge.inria.fr/bedwyr}}
250: and the user manual for Bedwyr \cite{baelde06manual} for more details about
251: these and other examples.
252:
253: {\em Finite failure}. Let $\false$ be an atom that
254: has no definition. Negation of a level-0 formula $G$ can then be
255: written as the level-1 formula $G\supset\false$ and this negation is
256: provable in the level-1 prover if all attempts to prove $G$ in the
257: level-0 prover fail. For example, the formula $\forall y [\lambda
258: x.x = \lambda x.y \supset \false]$ is a theorem: {\em i.e.}, the
259: identity abstraction is always different from a constant-valued
260: abstraction.
261:
262: {\em Model-checking}.
263: If the two predicates $P$ and $Q$ are defined using Horn clauses, then
264: the Level-1 prover is capable of attempting a proof of
265: $\forall x.~ P~x\supset Q~x$.
266: This covers most (un)reachability checks common in model-checking.
267: Related examples in the Bedwyr distribution include the verification of a 3 bits
268: addition circuit and graph cyclicity checks.
269:
270: {\em Games and strategies.}
271: Assuming that a transition in a game from position $P$ to position
272: $P'$ can be described by a level-0 formula $\step{P}{P'}$ then
273: proving the level-1 atom $\win P$ defined by
274: \[
275: \win P\defeq\forall P'.~\step P{P'}\supset\exists P''.~\step{P'}{P''}\land\win{P''}
276: \]
277: will determine if there is a winning strategy from position $P$. If
278: all {\sl win}-atoms are tabled during proof search, the resulting table
279: contains an actual winning strategy.
280:
281: {\em Simulation in process calculi.}
282: If the level-0 atom $\one{P}{A}{Q}$ specifies a one-step
283: transition (process $P$ does an $A$-action and results in process
284: $Q$), then simulation can be written in Bedwyr as follows \cite{mcdowell03tcs}.
285: \[
286: \simm P Q\defeq\forall A\forall P'.
287: ~\one{P}{A}{P'}\supset\exists Q'.\;\one{Q}{A}{Q'}\land\simm{P'}{Q'}
288: \]
289: In dealing with the $\pi$-calculus, where bindings can occur within
290: one-step transitions, there are two additional transitions that need
291: to be encoded: in particular, $\onep{P}{\downarrow X}{P'}$ and
292: $\onep{P}{\uparrow X}{P'}$, for bound input and bound output
293: transitions on channel $X$. In both of these cases, $P$ is a process
294: but $P'$ is a name abstraction over a process. The full specification
295: of (late, open) simulation for the $\pi$-calculus can be written using
296: the following \cite{miller05tocl}.
297: \[
298: \simm{P}{Q}\defeq
299: \begin{array}[t]{l}
300: [\forall A\forall P'
301: \begin{array}[t]{l}
302: .\;\one{P}{A}{P'}\supset\exists Q'.\;\one{Q}{A}{Q'}
303: \land \simm{P'}{Q'}]\land\null
304: \end{array} \\ \relax
305: [\forall X\forall P'
306: \begin{array}[t]{l}
307: .\;\onep{P}{\downarrow X}{P'}\supset
308: \exists Q'.\;\onep{Q}{\downarrow X}{Q'}
309: \land \forall w.\simm{(P'w)}{(Q' w)}]\land \null
310: \end{array} \\ \relax
311: [\forall X \forall P'
312: \begin{array}[t]{l}
313: .\;\onep{P}{\uparrow X}{P'}\supset\exists Q'.\;\onep{Q}{\uparrow X}{Q'}
314: \null\land\nabla w. \simm{(P' w)}{(Q' w)}]
315: \end{array}
316: \end{array}
317: \]
318: Notice that the abstracted continuation resulting from bound input and
319: bound output actions are treated by the $\forall$-quantifier and the
320: $\nabla$-quantifier, respectively. In a similar way, modal logics for
321: the $\pi$-calculus can be captured \cite{tiu05concur}.
322: If {\sl sim}-atoms are tabled during proof search, the resulting table
323: contains an actual simulation. Bisimulation is easily captured by
324: simply adding the symmetric clauses for all those used to define {\sl sim}.
325:
326:
327: {\em Meta-level reasoning}.
328: Because Bedwyr uses the $\nabla$ quantifier and the $\lambda$-tree approach to encoding syntax,
329: it is possible to specify provability in an object logic
330: and to reason to some extent about what is and is not provable.
331: Consider the tiny fragment of intuitionistic logic with the universal
332: quantifier $\overline \forall$ and the implication $\Rightarrow$ in which
333: we only allow atoms to the left of implications.
334: If the formula
335: $\overline\forall x.~(p~x~r\Rightarrow \overline\forall y.~(p~y~s\Rightarrow p~x~t))$
336: is provable in this logic then one would expect $r$ and $t$ to be syntactically
337: equal terms. In searching for a proof of this formula, the quantified variables are
338: replaced by distinct eigenvariables: therefore, the only way the formula could
339: have been proved is for $p~x~t$ to match $p~x~r$, hence $r = t.$
340: Provability of a formula $B$ from a list of atomic formulas $L$
341: can be specified by the following meta-level (Bedwyr-level) judgment $pv~L~B$:
342: \[
343: \begin{array}{l}
344: pv~L~B \defeq memb~B~L. \qquad\qquad\qquad
345: pv~L~(\overline\forall B) \defeq \nabla x.~pv~L~(B\,x).\\
346: pv~L~(A \Rightarrow B) \defeq pv~(A::L)~B.
347: \end{array}
348: \]
349: Here, $memb$ and $::$ are the usual predicate for list membership and
350: the non-empty list constructor. Object-level eigenvariables are
351: specified using the meta-level $\nabla$-quantifier.
352: The above observation about object-logic provability can now be stated
353: in the meta-logic as the following formula, which is provable in Bedwyr:
354: $$\forall r\forall s \forall t.~
355: pv~nil~(\overline\forall x.~(p~x~r\Rightarrow
356: \overline\forall y.~(p~y~s\Rightarrow p~x~t)))
357: \supset r = t.$$
358:
359:
360: \section{Future Work}
361:
362: We are working on several improvements to Bedwyr, including more
363: sophisticated tabling and allowing the suspension of goals containing
364: non-higher-order-pattern unification (rescheduling them when
365: instantiations change them into higher-order pattern goals).
366: We will also explore using tables as proof certificates: for example,
367: when proving that two processes are bisimilar, the table stores an
368: actual bisimulation, the existence of which proves the bisimilarity.
369: Bedwyr is an open source project: more details about it can be found at
370: {\tt \url{http://slimmer.gforge.inria.fr/bedwyr/}}.
371:
372: \paragraph{Acknowledgments.}
373: Support has been obtained for this work from the following
374: sources: from INRIA through the ``Equipes Associ{\'e}es'' Slimmer,
375: from the ACI grant GEOCAL, from the NSF Grants OISE-0553462
376: (IRES-REUSSI) and CCR-0429572 and from a grant from Boston Scientific.
377:
378: \bibliographystyle{plain}
379:
380: \begin{thebibliography}{10}
381:
382: \bibitem{baelde06manual}
383: David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu.
384: \newblock {\em A User Guide to {Bedwyr}}, November 2006.
385:
386: \bibitem{elliott91semi}
387: Conal Elliott and Frank Pfenning.
388: \newblock A semi-functional implementation of a higher-order logic programming
389: language.
390: \newblock In Peter Lee, editor, {\em Topics in Advanced Language
391: Implementation}, pages 289--325. MIT Press, 1991.
392:
393: \bibitem{girard92mail}
394: Jean-Yves Girard.
395: \newblock A fixpoint theorem in linear logic.
396: \newblock An email posting to the mailing list linear@cs.stanford.edu, February
397: 1992.
398:
399: \bibitem{mcdowell97lics}
400: Raymond McDowell and Dale Miller.
401: \newblock A logic for reasoning with higher-order abstract syntax.
402: \newblock In {\em Proc. LICS 1997}, pp. 434--445, IEEE Comp. Soc.
403: Press, 1997.
404:
405: \bibitem{mcdowell03tcs}
406: Raymond McDowell, Dale Miller, and Catuscia Palamidessi.
407: \newblock Encoding transition systems in sequent calculus.
408: \newblock {\em Theoretical Computer Science}, 294(3):411--437, 2003.
409:
410: \bibitem{miller00cl}
411: Dale Miller.
412: \newblock Abstract syntax for variable binders: An overview.
413: \newblock In John Lloyd and {et. al.}, editors, {\em Computational Logic - {CL}
414: 2000}, number 1861 in LNAI, pages 239--253. Springer, 2000.
415:
416: \bibitem{miller05tocl}
417: Dale Miller and Alwen Tiu.
418: \newblock A proof theory for generic judgments.
419: \newblock {\em ACM Trans.\ on Computational Logic}, 6(4):749--783, October
420: 2005.
421:
422: \bibitem{nadathur05iclp}
423: Gopalan Nadathur and Natalie Linnell.
424: \newblock Practical higher-order pattern unification with on-the-fly raising.
425: \newblock In {\em {ICLP 2005: 21st International Logic Programming
426: Conference}}, volume 3668 of {\em LNCS}, pages 371--386, Sitges, Spain,
427: 2005. Springer.
428:
429: \bibitem{pfenning88pldi}
430: Frank Pfenning and Conal Elliott.
431: \newblock Higher-order abstract syntax.
432: \newblock In {\em Proceedings of the {ACM}-{SIGPLAN} Conference on Programming
433: Language Design and Implementation}, pages 199--208. ACM Press, June 1988.
434:
435: \bibitem{sagonas06xsb}
436: Konstantinos Sagonas, Terrance Swift, David~S. Warren, Juliana Freire, Prasad
437: Rao, Baoqiu Cui, Ernie Johnson, Luis de~Castro, Rui~F. Marques, Steve Dawson,
438: and Michael Kifer.
439: \newblock {\em The {XSB} Version 3.0 Volume 1: Programmer's Manual}, 2006.
440:
441:
442: \bibitem{schroeder-heister93lics}
443: Peter Schroeder-Heister.
444: \newblock Rules of definitional reflection.
445: \newblock In {\em Proc. LICS 1993}, pages 222--232. IEEE Comp. Soc. Press, 1993.
446:
447: \bibitem{tiu04phd}
448: Alwen Tiu.
449: \newblock {\em A Logical Framework for Reasoning about Logical Specifications}.
450: \newblock PhD thesis, Pennsylvania State University, May 2004.
451:
452: \bibitem{tiu05concur}
453: Alwen Tiu.
454: \newblock Model checking for $\pi$-calculus using proof search.
455: \newblock In M. Abadi and L. de~Alfaro, editors, {\em CONCUR},
456: volume 3653 of {\em LNCS}, pages 36--50. Springer, 2005.
457:
458: \bibitem{tiu05eshol}
459: Alwen Tiu, Gopalan Nadathur, and Dale Miller.
460: \newblock Mixing finite success and finite failure in an automated prover.
461: \newblock In {\em Proc. of ESHOL'05: Empirically Successful Automated
462: Reasoning in Higher-Order Logics}, pages 79 -- 98, December 2005.
463:
464: \end{thebibliography}
465:
466: \end{document}
467: