Intelligence 2E

foundations of computational agents

The base language can be changed by modifying the meta-interpreter. The set of provable consequences can be enlarged by adding clauses to the meta-interpreter. The set of provable consequences can be reduced by adding conditions to the meta-interpreter clauses.

In all practical systems, not every predicate is defined by clauses. For example, it would be impractical to axiomatize arithmetic on current machines that can do arithmetic quickly. Instead of axiomatizing such predicates, it is better to call the underlying system directly. Assume the predicate $call(G)$ evaluates $G$ directly. Writing $call(p(X))$ is the same as writing $p(X)$. The predicate $call$ is required because the definite clause language does not allow free variables as atoms.

Built-in procedures can be evaluated at the base level by defining the meta-level relation $built\mathrm{\_}in(X)$ that is true if all instances of $X$ are to be evaluated directly; $X$ is a meta-level variable that must denote a base-level atom. Do not assume that “$built\mathrm{\_}in$” is provided as a built-in relation. It can be axiomatized like any other relation.

The base language can be expanded to allow for disjunction in the body of a clause, where the disjunction, $A\vee B$, is true in an interpretation $I$ when either $A$ is true in $I$ or $B$ is true in $I$ (or both are true in $I$). Allowing disjunction in the body of base-level clauses does not require disjunction in the metalanguage.

Figure 14.11 shows a meta-interpreter that allows built-in procedures to be evaluated directly and allows disjunction in the bodies of rules. This requires a database of built-in assertions and assumes that $call(G)$ is a way to prove $G$ in the meta-level.

An example of the kind of base-level rule the meta-interpreter of Figure 14.11 can now interpret is

${c}{}{a}{}{n}{}{\mathrm{\_}}{}{s}{}{e}{}{e}{\Leftarrow}{}{e}{}{y}{}{e}{}{s}{}{\mathrm{\_}}{}{o}{}{p}{}{e}{}{n}{\&}{(}{l}{}{i}{}{t}{}{(}{{l}}_{{1}}{)}{\vee}{l}{}{i}{}{t}{}{(}{{l}}_{{2}}{)}{)}{.}$ |

which says that ${c}{\mathit{}}{a}{\mathit{}}{n}{\mathit{}}{\mathrm{\_}}{\mathit{}}{s}{\mathit{}}{e}{\mathit{}}{e}$ is true if ${e}{\mathit{}}{y}{\mathit{}}{e}{\mathit{}}{s}{\mathit{}}{\mathrm{\_}}{\mathit{}}{o}{\mathit{}}{p}{\mathit{}}{e}{\mathit{}}{n}$ is true and either ${l}{\mathit{}}{i}{\mathit{}}{t}{\mathit{}}{\mathrm{(}}{{l}}_{{\mathrm{1}}}{\mathrm{)}}$ or ${l}{\mathit{}}{i}{\mathit{}}{t}{\mathit{}}{\mathrm{(}}{{l}}_{{\mathrm{2}}}{\mathrm{)}}$ is true (or both).

% $prove(G)$ is true if base-level body $G$ is a logical consequence of the base-level knowledge base.

$prove(true).$ | ||

$prove((A\&B))\leftarrow $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}prove(A)\wedge $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}prove(B).$ | ||

$prove((A\vee B))\leftarrow $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}prove(A).$ | ||

$prove((A\vee B))\leftarrow $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}prove(B).$ | ||

$prove(H)\leftarrow $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}built\mathrm{\_}in(H)\wedge $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}call(H).$ | ||

$prove(H)\leftarrow $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}(H\Leftarrow B)\wedge $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}prove(B).$ |

Given such an interpreter, the meta-level and the base level are different languages. The base level allows disjunction in the body. The meta-level does not require disjunction to provide it for the base language. The meta-level requires a way to interpret $call(G)$, which the base level cannot handle. The base level, however, can be made to interpret the command $call(G)$ by adding the following meta-level clause:

$prove(call(G))\leftarrow $ | ||

$\mathrm{}\mathit{\hspace{1em}\hspace{1em}\u2006}prove(G).$ |