4.4.4 · Operational limits of logic programming

Closed-world negation requires a complete fact boundary.

A query system gives mathematical-looking rules an operational search procedure. Missing facts and termination bounds shape what a run can conclude.

Guiding question

Which conclusions come from the logical relation, and which come from the particular database and search procedure?

Distinguish logical negation from negation as failure
State the closed-world assumption required by a missing-fact conclusion
Separate a relation’s declarative meaning from its search procedure
Observe a symmetric rule prove one query and loop on another
Use a visible work bound instead of presenting nontermination as an answer

The first program deliberately defines not-known-role? as failure to find a role fact. It returns true for ada, cy, and zoe. Ada and cy are known people whose manager role is absent, while zoe is absent from the known-person relation. A closed-world database boundary turns each failed lookup into logical negation.

The second program gives married a symmetric operational rule: when a direct fact is absent, swap the arguments and search again. This proves (married mickey minnie) after one swap because the reverse fact exists. The same rule alternates forever for an unrelated pair unless the evaluator detects repetition or spends a visible work budget. The logical statement may be symmetric, but the direction and control of the rule still determine the behavior of this executable search.

SICP code971 of 1,048,576 UTF-8 bytes

(begin
  (define facts
    '((known-person ada)
      (known-person ben)
      (known-person cy)
      (role ada programmer)
      (role ben manager)))
  (define (fact? candidate remaining)
    (cond ((null? remaining) #f)
          ((equal? candidate (car remaining)) #t)
          (else (fact? candidate (cdr remaining)))))
  (define (known-person? person)
    (fact? (list 'known-person person) facts))
  (define (known-role? person role)
    (fact? (list 'role person role) facts))
  (define (not-known-role? person role)
    (not (known-role? person role)))
  (define (role-status person role)
    (cond ((known-role? person role) 'proved)
          ((known-person? person) 'not-proved-for-known-person)
          (else 'unknown-person)))
  (list (not-known-role? 'ada 'manager)
        (not-known-role? 'cy 'manager)
        (not-known-role? 'zoe 'manager)
        (role-status 'ada 'manager)
        (role-status 'cy 'manager)
        (role-status 'zoe 'manager)))

Examples

Result—

Output: —
Value: —
Diagnostic: —

Execution trace0 / 0 events

Expected result

The first program returns (#t #t #t not-proved-for-known-person not-proved-for-known-person unknown-person). The second returns ((proved ((mickey minnie) (minnie mickey)) 3) (truncated ((donald daisy) (daisy donald) (donald daisy) (daisy donald) (donald daisy)) 0)).

Trace focus

In the first run, compare the three identical failed-role booleans with the separate known-person checks that preserve different epistemic states. In the second, follow each argument swap, direct fact scan, path extension, and budget decrease. One query reaches a fact after one swap; the other repeats the same two pairs until the explicit bound reports truncation.

Try it yourself

Change the program and compare the result.

Add (known-person zoe) without adding a role, then add (married daisy donald). Predict which status changes in the first run and which symmetric query now completes in the second.

Show hint

Adding a known-person fact changes zoe from an unknown person to a known person with no recorded role. Adding the direct married fact gives the reversed query a one-swap derivation path.

Complete this lesson

0 of 23 lessons complete in this chapter0%