Nixon Diamond

Two rules of thumb disagree about one person: which one wins, and why.

nixon-diamond.py · output · proof · check · try it in the playground

The question

A default is a rule of thumb: it holds unless something says otherwise. In this fictional rulebook, Quakers are pacifists by default, and Republicans are nonpacifists. The rulebook also says which rule wins when they clash: the Republican one.

Nixon is both a Quaker and a Republican. Ada is only a Quaker. (The names and memberships are made up for the example; they say nothing about anyone’s real beliefs.)

Drawn as a picture, Nixon sits at the bottom of a diamond with one path up to pacifist and one to nonpacifist: hence the name.

Is Nixon a pacifist? Is Ada?

What we tell eyekind

fact(quaker('nixon'))
fact(republican('nixon'))
fact(quaker('ada'))

implies([quaker(Person), not_(nonpacifist(Person))], pacifist(Person))
implies(republican(Person), nonpacifist(Person))

implies(quaker(Person), classification(Person, 'quaker'))
implies(republican(Person), classification(Person, 'republican'))
implies(pacifist(Person), classification(Person, 'pacifist'))
implies(nonpacifist(Person), classification(Person, 'nonpacifist'))

query(classification(Person, Class))

The first three lines are facts: things we simply state as true.

implies(condition, conclusion) is a rule: whenever the condition holds, eyekind concludes the conclusion. A list in square brackets means all of these. Person and Class are variables: capitalized placeholders that can stand for anyone.

The first rule is the default, with a guard: not_(nonpacifist(Person)) reads “nothing concludes that this person is a nonpacifist”. So a Quaker is a pacifist unless the nonpacifist rule says otherwise. That guard is what gives the Republican rule priority.

The four classification rules collect every label a person receives, and query(...) asks eyekind to report all of them.

The default waits its turn

A rule that says “nothing concludes X” must not be used too early: if it ran before the nonpacifist rule, it would wrongly find nothing.

eyekind therefore sorts the rules into layers, called strata. The rules that can conclude nonpacifist form an earlier layer; the default, which looks for the absence of nonpacifist, runs only after that layer has finished. This is stratified negation: “not found” is only asked once all the contrary evidence is in.

What eyekind concludes

// Answers: each instance of a query() that holds.
classification('nixon', 'quaker')
classification('ada', 'quaker')
classification('nixon', 'republican')
classification('nixon', 'nonpacifist')
classification('ada', 'pacifist')

The comment line says what follows: the filled-in versions of the question that are true.

Nixon is a Quaker, a Republican and a nonpacifist, and not a pacifist: the Republican rule made him a nonpacifist, and the guard then blocked the default.
Ada is a Quaker and, with nothing against her, gets the default: she is a pacifist.

The proof, line by line

eyekind --proof writes down how it reached each answer. This is the complete proof:

// Answers: each instance of a query() that holds.
classification('nixon', 'quaker')
classification('ada', 'quaker')
classification('nixon', 'republican')
classification('nixon', 'nonpacifist')
classification('ada', 'pacifist')

// Clauses: the program clauses the steps cite, by clause number.
clause(1, fact(quaker('nixon')))
clause(2, fact(republican('nixon')))
clause(3, fact(quaker('ada')))
clause(4, implies([quaker(Person), not(nonpacifist(Person))], pacifist(Person)))
clause(5, implies(republican(Person), nonpacifist(Person)))
clause(6, implies(quaker(Person), classification(Person, 'quaker')))
clause(7, implies(republican(Person), classification(Person, 'republican')))
clause(8, implies(pacifist(Person), classification(Person, 'pacifist')))
clause(9, implies(nonpacifist(Person), classification(Person, 'nonpacifist')))

// Steps: each goal, what justifies it (a clause, a builtin, a control, or an
// absence or collection taken on trust), the bindings and the goals it uses.
step(classification('nixon', 'quaker'), clause(6), {Person: 'nixon'}, [quaker('nixon')])
step(quaker('nixon'), clause(1), {}, [])
step(classification('ada', 'quaker'), clause(6), {Person: 'ada'}, [quaker('ada')])
step(quaker('ada'), clause(3), {}, [])
step(classification('nixon', 'republican'), clause(7), {Person: 'nixon'}, [republican('nixon')])
step(republican('nixon'), clause(2), {}, [])
step(classification('nixon', 'nonpacifist'), clause(9), {Person: 'nixon'}, [nonpacifist('nixon')])
step(nonpacifist('nixon'), clause(5), {Person: 'nixon'}, [republican('nixon')])
step(classification('ada', 'pacifist'), clause(8), {Person: 'ada'}, [pacifist('ada')])
step(pacifist('ada'), clause(4), {Person: 'ada'}, [quaker('ada'), not(nonpacifist('ada'))])
step(not(nonpacifist('ada')), 'absent', {}, [])

It has three parts:

The claims: the five answers the proof is about.
The clauses: the program’s facts and rules, numbered in program order.
The steps: one per thing established. A step reads step(what, by what, with which values, using what). The values say who Person stood for; using what lists the things the step needs, each with a step of its own.

Two kinds of justification occur:

clause(N): the step is an instance of fact or rule N.
'absent': the step says that something could not be found. Nothing can be shown for a missing fact, so this step is taken on trust: it is an obligation, a promise the checker records rather than proves.

Read the steps as sentences:

Nixon is classified as a Quaker — by rule 6, with Person = nixon, because Nixon is a Quaker.
Nixon is a Quaker — fact 1.
Ada is classified as a Quaker — by rule 6, with Person = ada, because Ada is a Quaker.
Ada is a Quaker — fact 3.
Nixon is classified as a Republican — by rule 7, because Nixon is a Republican.
Nixon is a Republican — fact 2.
Nixon is classified as a nonpacifist — by rule 9, because Nixon is a nonpacifist.
Nixon is a nonpacifist — by rule 5, because Nixon is a Republican (step 6).
Ada is classified as a pacifist — by rule 8, because Ada is a pacifist.
Ada is a pacifist — by the default, rule 4, because Ada is a Quaker (step 4) and nothing says she is a nonpacifist.
Nothing says Ada is a nonpacifist — absent: eyekind looked, after the nonpacifist rule had finished, and found nothing.

There is no step for “Nixon is a pacifist”: the default could not fire for him, because step 8 makes him a nonpacifist.

Checked: what the report says

A proof is only worth something if someone else can check it. eyekind -c generates the proof and checks it against the program; --check-proof checks a saved proof. The checker never reasons by itself: it only confirms each step against the program. This is the complete report:

// Answers checked subject to the obligations below.
classification('nixon', 'quaker')
classification('ada', 'quaker')
classification('nixon', 'republican')
classification('nixon', 'nonpacifist')
classification('ada', 'pacifist')

// C1-C8: resolution, acyclicity, justification, coverage,
// re-decision, boundary consistency, relevance and witness integrity.
condition('C1', 'resolution', 'ok', 10)
condition('C2', 'well_founded', 'ok', 11)
condition('C3', 'justification', 'ok', 11)
condition('C4', 'coverage', 'ok', 13)
condition('C5', 're_decision', 'ok', 0)
condition('C6', 'boundary_consistency', 'ok', 1)
condition('C7', 'relevance', 'ok', 16)
condition('C8', 'witness_integrity', 'ok', 0)

// Obligations: absence and collection completeness are taken on trust.
obligation('absent', 'theory_scoped', not(nonpacifist('ada')))

// Proof statistics: recorded steps and how they were checked.
steps(11)
verified(10)
recomputed(0)
composed(0)
trusted(1)
claims(5)

// This verdict applies to the claims above; it does not establish completeness.
verdict('checked_with_obligations')

Each condition line names a check, says 'ok', and counts what it looked at:

C1 resolution (10): the 10 steps that cite a clause really are instances of it. Step 10, for example, is rule 4 with Person = ada.
C2 well-founded (11): none of the 11 steps depends on itself, even indirectly.
C3 justification (11): every step says how it was justified, in a form the checker understands.
C4 coverage (13): the 5 claims and the 8 things the steps use are each backed by a step.
C5 re-decision (0): there was no calculation or built-in test to redo.
C6 boundary consistency (1): the 1 absence, nothing says Ada is a nonpacifist, was confronted with the evidence in the proof. No step concludes nonpacifist('ada'), so nothing refutes it.
C7 relevance (16): each of the 5 claims answers the question, and all 11 steps serve a claim.
C8 witness integrity (0): no rule invented a new, unnamed thing, so there is no invented name to verify.

The obligation line spells out what was taken on trust: an 'absent' step, that nonpacifist('ada') cannot be concluded. 'theory_scoped' means the absence is relative to this program: with these facts and rules, nothing makes Ada a nonpacifist. A different rulebook could.

The statistics repeat this: 11 steps, 10 verified against the program, 1 trusted. The verdict is checked with obligations: every answer follows from the program, provided that the absence really holds. As the last comment says, the verdict does not establish completeness: it does not say these are the only classifications there could be.

Try it

eyekind examples/nixon-diamond.py
eyekind --check-proof examples/proof/nixon-diamond.py examples/nixon-diamond.py
eyekind --proof examples/nixon-diamond.py
eyekind -c examples/nixon-diamond.py

Delete the line fact(republican('nixon')) and run again: nothing blocks the default any more, and Nixon is classified as a pacifist, like Ada. The check report now lists two absences, one for each of them.

Or remove the guard: replace the default with implies(quaker(Person), pacifist(Person)). Nixon is then classified as both a pacifist and a nonpacifist. eyekind does not object to the clash, because nothing in the program says the two cannot go together; and with no absence left, the verdict becomes plain checked.

Takeaway

When defaults conflict, decide which one wins and write it down. A guarded default makes the priority explicit, and the proof shows exactly which “nothing found” each conclusion leans on.