Failure to find a proof is not the same as proving a negation.
A query system gives mathematical-looking rules an operational search procedure. Missing facts, rule direction, database assumptions, and termination bounds therefore affect what a run can honestly conclude.
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. Those results do not carry the same information: ada and cy are known people whose manager role was not recorded, while zoe is not represented as a known person at all. Treating every failed lookup as a logical negation requires a closed-world claim that the database contains every relevant fact.
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.
(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)))- Output
- —
- Value
- —
- Diagnostic
- —
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)).
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.
Change the program before you read the hint.
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 one hint
Adding a known-person fact changes what the database can say about zoe without proving a role. Adding the direct married fact gives the reversed query a one-swap proof path.