Queries

There are two kinds of queries in Celf: #query directives to find inhabitants of a type and #exec or #trace directives to explore the behavior of an evolving system.

All the examples in this section use this 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}.

Query directives

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 to find a proof term showing that the type ty is inhabited.

Argument 4 - Number of attempts

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.

Argument 1 - Bound on forward-chaining steps

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.

Argument 2 - Expected number of solutions

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

Argument 3 - Number of solutions to look for

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

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

The files tests/change.clf and tests/lambda-env.clf in the source are designed to demonstrate the use of #trace and #exec.