In order to establish a query from the facts already established in the system, the query interpreter performs a search in the space of all possible facts. Unification is the primitive operation that pattern matches two expressions. The search procedure in a query interpreter chooses what expressions to unify in order to find a set of facts that chain together to establishes the query.

The recursive search function implements the search procedure for the logic language. It takes as input the Scheme list of clauses in the query, an environment env containing current bindings of symbols to values (initially empty), and the depth of the chain of rules that have been chained together already.

>>> def search(clauses, env, depth):
            """Search for an application of rules to establish all the CLAUSES,
            non-destructively extending the unifier ENV.  Limit the search to
            the nested application of DEPTH rules."""
            if clauses is nil:
                yield env
            elif DEPTH_LIMIT is None or depth <= DEPTH_LIMIT:
                if clauses.first.first in ('not', '~'):
                    clause = ground(clauses.first.second, env)
                    try:
                        next(search(clause, glob, 0))
                    except StopIteration:
                        env_head = Frame(env)
                        for result in search(clauses.second, env_head, depth+1):
                            yield result
                else:
                    for fact in facts:
                        fact = rename_variables(fact, get_unique_id())
                        env_head = Frame(env)
                        if unify(fact.first, clauses.first, env_head):
                            for env_rule in search(fact.second, env_head, depth+1):
                                for result in search(clauses.second, env_rule, depth+1):
                                    yield result
    

The search to satisfy all clauses simultaneously begins with the first clause. In the special case where our first clause is negated, rather than trying to unify the first clause of the query with a fact, we check that there is no such unification possible through a recursive call to search. If this recursive call yields nothing, we continue the search process with the rest of our clauses. If unification is possible, we fail immediately.

If our first clause is not negated, then for each fact in the database, search attempts to unify the first clause of the fact with the first clause of the query. Unification is performed in a new environment env_head. As a side effect of unification, variables are bound to values in env_head.

If unification is successful, then the clause matches the conclusion of the current rule. The following for statement attempts to establish the hypotheses of the rule, so that the conclusion can be established. It is here that the hypotheses of a recursive rule would be passed recursively to search in order to be established.

Finally, for every successful search of fact.second, the resulting environment is bound to env_rule. Given these bindings of values to variables, the final for statement searches to establish the rest of the clauses in the initial query. Any successful result is returned via the inner yield statement.

Unique names. Unification assumes that no variable is shared among both e and f. However, we often reuse variable names in the facts and queries of the logic language. We would not like to confuse an ?x in one fact with an ?x in another; these variables are unrelated. To ensure that names are not confused, before a fact is passed into unify, its variable names are replaced by unique names using rename_variables by appending a unique integer for the fact.

>>> def rename_variables(expr, n):
            """Rename all variables in EXPR with an identifier N."""
            if isvar(expr):
                return expr + '_' + str(n)
            elif scheme_pairp(expr):
                return Pair(rename_variables(expr.first, n),
                            rename_variables(expr.second, n))
            else:
                return expr
    

The remaining details, including the user interface to the logic language and the definition of various helper functions, appears in the logic example.