%query

The %query declarations specify a type (that corresponds to a judgment by the judgments as types principle), and tells STELF’s logic programming engine to search for a proof of that judgment.

A query declaration also takes two other inputs, which can either be a number or a star “*”. The meaning of this is a bit awkward and counterintuitive:

• The first input is the expected number of solutions - a star here means “as many solutions as you let STELF look for”
• The second input is the number of solutions to find - a star here means “keep looking until you have found all solutions”

This means that some possible queries will always fail:

• %query 5 4 ... will always fail because there is no way to come up with 5 solutions in 4 tries
• %query 6 6 ... means the same thing as %query * 6 ..., because both mean “try six times, and find a solution every time”
• %query * * ... will either keep coming up with more solutions forever (and will therefore not terminatie) or it will eventually fail to come up with a solution and so will fail.

It also means there are often multiple ways to write the same query, as the examples below demonstrate.

Examples

We will use the example of list membership to demonstrate %query because there may be multiple ways to find an element in a list (if that element occurs multiple times).

%sort elem %.
%term a elem %.
%term b elem %.
%term c elem %.
%term d elem %.
%sort list %.
%term nil list %.
%term , %pi elem %-> list %-> list %.
%prec %right 10 , %.
%define sample-list list a , c , a , b , a , c , a , a , b , c , c , d , nil %.
%sort member {_ elem} {_ list} %.
%term member/hit member A (A , L) %.
%term member/skip %pi (member A (B , L)) %<- (member A L) %.

Confirming there is one “d” in the list

%query 1 * member d sample-list.

Confirming there are at least three “a’s” in the list

%query 3 3 member a sample-list.

Confirming there are at least two “b’s” in the list

%query * 2 member b sample-list.

Confirming there are at least zero “c’s” in the list (the query isn’t even run)

%query * 0 member c sample-list.   %

Confirming there are at least zero “c’s” in the list (the query isn’t even run)

%query 8 0 member c sample-list.

Confirming there are three “a’s” in the list (fails, there are more)

%query 3 * member a sample-list.

Getting output from %query

Unlike %solve, %query declarations do not allow you to insert the output of a query into the signature. However, you can inspect the output in the STELF buffer. For example, if we leave the first argument of %query as a TODO, the following query will output the first two elements it finds in the list (the first two elements in the list).

%query _ 2 _ member E sample-list %.

Furthermore, if you change the format of a query from %query 1 * ... to %query 1 * D : ..., where D is some uppercase identifier, it will print the TODO that caused the query to succeed. The proof terms below indicate that the first two instances of b is located in the fourth position in the list (the search skips three times and then hits) and in the ninth position in the list (the search skips eight times and then hits).

%query _ 2 _ %the (member b sample-list) D %.

See also

• Query Declaration (guide §5.23)