# Queries

##### Clone this wiki locally

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)

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`.