-
Notifications
You must be signed in to change notification settings - Fork 5
Queries
There are two kinds of queries in Celf: #query
directives and #exec
or #trace
directives.
All the examples in this section use the following base code:
nat: type.
z: nat.
s: nat -> nat.
up: nat -> type.
down: nat -> type.
u: up N -o {up (s N)}.
d: down (s N) -o {down N}.
TL;DR - #query * * * 1 NEG-TYPE
and use the celf -hquery
if that doesn't do what you want.
Fundamentally, what #query d e l a ty.
does is perform a
attempts for a proof term of ty
.
The mandatory fourth argument NUM
represents the number of times to run the query. If you only specify this last argument, the result will be insensitive to the actual number of solutions proof search finds.
#query * * * 15 down z -o {down (s z)}. % 15 attempts, 0 solutions
#query * * * 2 down (s z) -o {down z}. % 2 attempts, 2 solutions (the same one)
badnat: nat.
d': down (s (s z)) -o {down badnat}.
#query * * * 100 down (s (s z)) -o {down z}. % 100 attempts, about 50 solutions
The first three arguments are optional either a number or the wildcard *
can be given. They are d
(bound on forward-chaining steps), e
(expected number of solutions), and l
(number of solutions to look for.
Intended to deal with some of the problems arising from unrestricted forward-chaining search. Usually forward chaining runs to quiescence - that is, until there is no more forward chaining possible. An alternative is to declare that forward chaining must always run for a fixed number of steps (no more and no fewer, as the last query below demonstrates).
#query * * * 1 down (s (s z)) -o {down z}. % 1 solution
#query 1 * * 1 down (s (s z)) -o {down z}. % 0 solutions
#query * * * 1 down (s (s z)) -o {down (s z)}. % 0 solutions
#query 1 * * 1 down (s (s z)) -o {down (s z)}. % 1 solution
#query 4 * * 1 up z -o {up (s (s (s (s (s z)))))}. % 0 solutions
#query 5 * * 1 up z -o {up (s (s (s (s (s z)))))}. % 1 solution
#query 6 * * 1 up z -o {up (s (s (s (s (s z)))))}. % 0 solutions
It's probably better to use #trace
or #exec
in these situations.
This argument can be used to make #query
directives fail and stop the file from loading; it specifies a minimum number of expected solutions. Since forward-chaining uses a pseudo-random number generator (which can be seeded with the -s
command line flag), this can give queries some probability of succeeding when given a nondeterministic specification.
badnat: nat.
d': down (s (s z)) -o {down badnat}.
#query * 1 * 100 down (s (s z)) -o {down z}. % Likely to succeed
#query * 1 * 1 down (s (s z)) -o {down z}. % 50/50 chance of failure
#query * 100 * 1 down (s (s z)) -o {down z}. % Always fails
This is the option to use if you want the familiar Prolog backtracking multiple-solutions semantics. If you use this option, the last argument (somewhat awkwardly) must be 1
.
lt: nat -> nat -> type.
ltz: lt z (s N).
lts: lt N M -o lt (s N) (s M).
#query * * 20 1 lt N (s (s (s (s (s (s z)))))). % Succeeds, 6 solutions
#query * 5 20 1 lt N (s (s (s (s (s (s z)))))). % Fails (too many solutions)
#query * 6 20 1 lt N (s (s (s (s (s (s z)))))). % Succeeds, 6 solutions
#query * 7 20 1 lt N (s (s (s (s (s (s z)))))). % Fails
Trace and exec directives have the same form: #trace ? POS-TYPE.
and #exec ? POS-TYPE.
where ?
is either a natural number NUM
or a wildcard *
. These directives decompose the type POS-TYPE
into the context and then perform monadic forward chaining for NUM
steps (if some maximum number is specified) or until quiescence is reached, whichever comes first, and reports what the end state was.
#exec * down (s (s (s (s (s z))))). % -- down z lin
#exec 3 down (s (s (s (s (s z))))). % -- down (s !(s !z)) lin
#exec 4 down (s (s (s (s (s z))))). % -- down (s !z) lin
#exec 5 down (s (s (s (s (s z))))). % -- down z lin
#exec 6 down (s (s (s (s (s z))))). % Fails (cannot take 6 steps)
The only difference between the two queries is that #trace
also reports intermediate steps; the result of running #trace 5 up z.
is that Celf outputs the following:
-- up z lin
-- up (s !z) lin
-- up (s !(s !z)) lin
-- up (s !(s !(s !z))) lin
-- up (s !(s !(s !(s !z)))) lin
-- up (s !(s !(s !(s !(s !z))))) lin