The Little Prover¶
This is an annotated version of [FE15], with examples coded in Smalltalk on top of the logic language µKanren. To drive the reader through the text, please keep in mind that the main flow is taken from the original text, the smallest amount of text to give it sense and I don’t deserve any merit for that. My own notes and additions will be emphasized in note boxes. Therefore, if you would like to stick to the book be free to skip notes, otherwise dig into them to get a deeper understanding of what’s new from our side.
Old Games, New Rules¶
Salutations. What are salutations? Salutations are a fancy way of saying
hello or good morning.
Thank you, D. Friedman and C. Eastlung.
What is (#ham cons: (#eggs cons: nil)) equal to?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_06
"(car (cons 'ham '(eggs)))"
self assert: (#ham cons: (#eggs cons: nil)) car equals: #ham
What value is the expression nil isAtom equal to?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_11
"(atom '())"
self assert: nil isAtom equals: true
Can we find a value for the expression (#ham cons: (#eggs cons: nil)) isAtom?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_14
"(atom (cons 'ham '(eggs)))"
self assert: (#ham cons: (#eggs cons: nil)) isAtom equals: false
Note
The selector #isAtom has two implementors, both
"Object, protocol *Collections-Sequenceable-Cons"
isAtom
^ true
and
"Cons, protocol testing"
isAtom
^ false
respectively. The latter is implemented in
Object subclass: #Cons
instanceVariableNames: 'car cdr'
classVariableNames: ''
package: 'Collections-Sequenceable-Cons'
that can be instantiated with
"Object, protocol *MicroKanren-core"
cons: anObj
^ anObj consedObject: self
"Object, protocol *Collections-Sequenceable-Cons"
consedObject: car
^ Cons car: car cdr: self
No matter what values the variables a and b have, the expression a
cons: b cannot produce an object c such that c isAtom evaluates to
true,
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_16
| aGoal |
aGoal := [ :rewrite |
[ :ast |
[ :a :b |
theory isAtomConsº value: ast value: rewrite asRBNode ] ]
asGoalWithUnaryASTof: [ :a :b | (a cons: b) isAtom ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { false asLiteralRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
where
"TheLittleProver, protocol predicates" isAtomConsº "(dethm atom/cons (x y) (equal (atom (cons x y)) 'nil))" ^ [ :x :y | (x cons: y) isAtom ] <~~> [ :x :y | false ]
Note
Wait. Many new things pop up here, so digest one at the time. In order of occurrence:
the message
"BlockClosure, protocol *MicroKanren-RB" asGoalWithUnaryASTof: aBlock contextVariables: aCollection ^ self asGoalWithASTof: aBlock contextVariables: aCollection select: [ :aSequenceNode | aSequenceNode statements in: [ :statements | statements size = 1 ifTrue: [ statements first ] ifFalse: [ Error signal: ('Assumption that {} has 1 statement only is violated.' format: { aSequenceNode }) ] ] ]
forwards, after ensuring that
aBlockhas exactly one statement, to"BlockClosure, protocol *MicroKanren-RB" asGoalWithASTof: aBlock contextVariables: aCollection select: selectBlock ^ FreshRB new receiver: aBlock; nodeBlock: self; selectBlock: selectBlock; contextVariables: aCollection; yourself
in order to produce a
FreshRBgoal that, overriding the message"FreshRB, protocol dispatched" onState: aState withVars: aCollection | dict node rbLogicVariables swapping aStream | dict := Dictionary new. contextVariables keysAndValuesDo: [ :aSymbol :aRBVar | dict at: aSymbol put: aRBVar ]. rbLogicVariables := receiver argumentNames with: aCollection collect: [ :aName :aVar | dict at: aName ifPresent: [ Error signal: ('Variable {} duplicated!' format: { aName }) ] ifAbsentPut: [ aVar asRBNode ] ]. node := receiver sourceNode body in: [ :aSequenceNode | | aNode | aNode := selectBlock value: aSequenceNode. aNode substituteVariablesUsingDictionary: dict ]. swapping := receiver. receiver := nodeBlock value: node. aStream := super onState: aState withVars: aCollection. receiver := swapping. ^ aStream
has the responsibility to lift block’s code variables
"RBNode, protocol *MicroKanren-RB" substituteVariablesUsingDictionary: aDict ^ self acceptVisitor: (RBProgramNodeSubstitutionVisitor new substitution: aDict; yourself)
"RBProgramNodeSubstitutionVisitor, protocol visiting" visitTemporaryNode: aNode ^ aNode isVariable ifTrue: [ substitution at: aNode name ] ifFalse: [ aNode ]
to
RBNodeobjects that support unificationRBVariableNode subclass: #RBLogicVariableNode instanceVariableNames: 'logicVar' classVariableNames: '' package: 'MicroKanren-RB'
via
"Var, protocol *MicroKanren-RB" asRBNode ^ RBLogicVariableNode named: named logicVar: self
lying on
Vareventually.the message
"Object, protocol *MicroKanren-RB" asLiteralRBNode ^ self isLiteral ifTrue: [ RBLiteralValueNode value: self ] ifFalse: [ Error signal: 'I am not a literal value' ]
allows us to lift a literal value to a literal node.
the message
"BlockClosure, protocol *MicroKanren-RB" <~~> aBlock ^ [ :a :b | [ :ast | [ :x :y | | z | z := aBlock substituteVariablesUsingSequenceableCollection: (Array with: x asRBNode with: y asRBNode). (ast unifyo value: a) , (z unifyo value: b) ] ] asGoalWithUnaryASTof: self contextVariables: #( ) ]
is syntactic sugar to define a rewriting rule upto α-conversion over names of variables of both blocks, implemented in
"BlockClosure, protocol *MicroKanren-RB" substituteVariablesUsingSequenceableCollection: rbVariables ^ self unaryRBNode substituteVariablesUsingDictionary: (self argumentNames with: rbVariables collect: #->) asDictionary
Such conversion if helpful to be free to use arbitrary names during a rewriting, as in
TheLittleProver>>#carConsºfor example.
As usual in logic, we can run a computation backward. The following test case
shows how to use #isAtomConsº to generate the receiver of #isAtom under
the constraint that the whole expression yields false when evaluated:
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_16_backward
| aGoal node |
aGoal := [ :ast |
[ :a |
theory isAtomConsº value: ast value: false asLiteralRBNode ] ]
asGoalWithUnaryASTof: [ :a | a isAtom ]
contextVariables: Dictionary empty.
node := [ :a :b | a cons: b ]
substituteVariablesUsingSequenceableCollection: {
0 asReifiedVar asRBNode.
1 asReifiedVar asRBNode }.
self
assert: aGoal solutions readStream upToEnd equals: { node };
assert: node formattedCode equals: '•₀ cons: •₁'.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
Note
Since a CompiledMethod responds to
"CompiledMethod, protocol *opalcompiler-core"
sourceNode
^ self ast
the initial test
TheLittleProverTest>>#test_chapter_01_OldGamesNewRules_frame_16_byBlockClosure
can also be written as
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_16_byCompiledMethod
| aGoal |
aGoal := [ :rewrite |
[ :ast | self consº: ast isAtomº: rewrite asRBNode ]
asGoalWithUnaryASTof: self class >> #consª:isAtomª:
contextVariables: #( ) ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { false asLiteralRBNode }
where, on one hand, code as data is
"TheLittleProverTest, protocol code as data"
consª: a isAtomª: b
(a cons: b) isAtom
on the other hand, the rewriting is
"TheLittleProverTest, protocol predicates"
consº: ast isAtomº: rewritten
^ [ :a :b | theory isAtomConsº value: ast value: rewritten ]
Observe that the previous two messages allow us to establish a nomenclature
for when we use a CompiledMethod both for its source code and for
evaluating (a predicate BlockClosure in this case) by appending a ª
and º to each keyword in the selector, respectively. This scheme has the
advantage to use the same words while being able to discriminate their usage.
We mix the two approaches freely from now on.
We want to focus on (a cons: b) isAtom in the context of the outer #= message send
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_19
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
ast
acl: [ :prover |
prover
focus: [ :o | #flapjack = o ]
do: theory isAtomConsº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :a :b |
#flapjack = (a cons: b) isAtom ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { [ #flapjack = false ] unaryRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
Note
The message
"BlockClosure, protocol *MicroKanren-RB"
unaryRBNode
^ self sourceNode body statements in: [ :statements |
statements size = 1
ifTrue: [ statements first ]
ifFalse: [
Error signal:
('Assumption that {} has 1 statement only is violated.'
format: { self }) ] ]
is helpful to use a BlockClosure object as a container of its own code.
Precisely. In that case, what value is #flapjack = false equal to?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_21
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
ast
acl: [ :prover |
prover
focus: [ :o | #flapjack = o ] do: theory isAtomConsº;
focus: [ :o | o ] do: self flapjackNilFalseº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :a :b |
#flapjack = (a cons: b) isAtom ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { false asLiteralRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
where
"TheLittleProverTest, protocol predicates" flapjackNilFalseº ^ [ :_ | #flapjack = false ] <~> [ :_ | false ]
What value is the expression ((p cons: q) car cons: nil) cdr isAtom equal to?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_28
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
ast
acl: [ :prover |
prover
focus: [ :o | (o cons: nil) cdr isAtom ]
do: theory carConsº;
focus: [ :o | o isAtom ] do: theory cdrConsº;
focus: [ :o | o ] do: theory isAtomNilº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :p :q |
((p cons: q) car cons: nil) cdr isAtom ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { true asLiteralRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
where
"TheLittleProver, protocol predicates" carConsº "(dethm car/cons (x y) (equal (car (cons x y)) x))" ^ [ :x :y | (x cons: y) car ] <~~> [ :a :b | a ]"TheLittleProver, protocol predicates" cdrConsº "(dethm cdr/cons (x y) (equal (cdr (cons x y)) y))" ^ [ :x :y | (x cons: y) cdr ] <~~> [ :x :y | y ]"TheLittleProver, protocol predicates" isAtomNilº " (dethm atom/nil (x y) (equal (atom 'nil) 't))" ^ [ :_ | nil isAtom ] <~> [ :_ | true ]
That took three steps. Can we do it in fewer?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_32
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
ast
acl: [ :prover |
prover
focus: [ :o | o isAtom ] do: theory cdrConsº;
focus: [ :o | o ] do: theory isAtomNilº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :p :q |
((p cons: q) car cons: nil) cdr isAtom ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { true asLiteralRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
What is the value of the context ((x cons: y) = (x cons: y) cons: (#and cons:
(#crumpets cons: nil))) car with focus on (x cons: y) = (x cons: y)?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_44
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
ast
acl: [ :rewrite |
rewrite
focus: [ :o |
(o cons: (#and cons: (#crumpets cons: nil))) car ]
do: theory equalSameº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :x :y |
((x cons: y) = (x cons: y) cons:
(#and cons: (#crumpets cons: nil))) car ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals:
{ [ (true cons: (#and cons: (#crumpets cons: nil))) car ]
unaryRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
And, of course, the second step is easy.
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_46
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
ast
acl: [ :rewrite |
rewrite
focus: [ :o |
(o cons: (#and cons: (#crumpets cons: nil))) car ]
do: theory equalSameº.
rewrite focus: [ :o | o ] do: theory carConsº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :x :y |
((x cons: y) = (x cons: y) cons:
(#and cons: (#crumpets cons: nil))) car ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { true asLiteralRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
Note
Please note that #equalSameº also binds variables during its evaluation
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_46_variablesBindingByEqualSame
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :car :cdr |
[ :r |
| g1 g2 |
g1 := theory equalSameº value: ast value: r asRBNode.
g2 := rewritten asRBNode unifyo value: (RBMessageNode
receiver: car asRBNode
selector: #cons:
arguments: { cdr asRBNode }).
g1 , g2 ] asGoal ] ]
asGoalWithUnaryASTof: [ :a :d |
(#and cons: d) = (a cons: nil) ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { [ #and cons: nil ] unaryRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
morever, variables binding can be performed manually as in
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_46_variablesBindingManually
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
(rewritten asRBNode unifyo value:
(RBMessageNode receiver: a asRBNode selector: #even))
, ((RBLiteralValueNode value: 3) unifyo value: a asRBNode) ] ]
asGoalWithUnaryASTof: [ :a :b | a + b ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { [ 3 even ] unaryRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
Does the order of the arguments to #= matter?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_49
| aGoal node |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
ast
acl: [ :rewrite |
rewrite focus: [ :o | o ] do: theory equalSwapº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :x :y |
(x cons: y) = (#bagels cons: (#and cons: (#lox cons: nil))) ]
contextVariables: Dictionary empty ] asGoal.
node := RBMessageNode
receiver:
[ (#bagels cons: (#and cons: (#lox cons: nil))) ]
unaryRBNode
selector: #=
arguments: { (RBMessageNode
receiver: 0 asReifiedVar asRBNode
selector: #cons:
arguments: { 1 asReifiedVar asRBNode }) }.
self
assert: aGoal solutions readStream upToEnd equals: { node };
assert: node formattedCode
equals:
'(#bagels cons: (#and cons: (#lox cons: nil))) = (•₀ cons: •₁)'.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
where
"TheLittleProver, protocol predicates" equalSwapº "(dethm equal-swap (x y) (equal (equal x y) (equal y x)))" ^ [ :x :y | x = y ] <~~> [ :x :y | y = x ]
What else the context y cons: (x cdr cons: y car) car = (x isAtom = false)
equal to with focus on (x cdr cons: y car) car according to #carConsº?
Recall that “is equal to” works in both directions.
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_55
| aGoal node |
aGoal := [ :rewritten |
[ :ast |
[ :a :b |
ast
acl: [ :rewrite |
rewrite
focus: [ :o | b cons: o = (a isAtom = false) ]
do: [ :o :r | theory carConsº value: r value: o ] ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: (Dictionary new
at: #a put: a asRBNode;
at: #b put: b asRBNode;
yourself) ] ]
asGoalWithUnaryASTof: [ :x :y |
y cons: (x cdr cons: y car) car = (x isAtom = false) ]
contextVariables: Dictionary empty ] asGoal.
node := self expectedRBNode_chapter_01_frame_55.
self
assert: aGoal solutions readStream upToEnd equals: { node };
assert: node formattedCode equals: '•₀ cons:
((•₁ cdr cons: •₀ car) car cons: •₂) car = (•₁ isAtom = false)'.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
Can we use TheLittleProver>>#carConsº, then
TheLittleProver>>#isAtomConsº and finally then
TheLittleProver>>#cdrConsº? And what value is the final expression equal to?
"TheLittleProverTest, protocol tests"
test_chapter_01_OldGamesNewRules_frame_56
| aGoal node |
aGoal := [ :rewritten |
[ :ast |
[ :x :y :a :b :c |
ast
acl: [ :rewrite |
rewrite
focus: [ :o | y cons: o = (x isAtom = false) ]
do: [ :o :r | theory carConsº value: r value: o ].
rewrite
focus: [ :o |
y cons:
((x cdr cons: y car) car cons: (#oats cons: nil)) car
= (x isAtom = o) ]
do: [ :o :r | theory isAtomConsº value: r value: o ].
rewrite
focus: [ :o |
y cons:
((x cdr cons: y car) car cons: (#oats cons: nil)) car
= (x isAtom = (o isAtom cons: (a cons: b) = c) isAtom) ]
do: [ :o :r | theory cdrConsº value: o value: r ].
rewrite
focus: [ :o |
y cons:
((x cdr cons: y car) car cons: (#oats cons: nil)) car
= (x isAtom = (b isAtom cons: o) isAtom) ]
do: [ :o :r | theory equalSwapº value: o value: r ] ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: (Dictionary new
at: #x put: x asRBNode;
at: #y put: y asRBNode;
at: #a put: a asRBNode;
at: #b put: b asRBNode;
at: #c put: c asRBNode;
yourself) ] ]
asGoalWithUnaryASTof: [ :x :y :a :b :c |
y cons: (x cdr cons: y car) car = (x isAtom = false) ]
contextVariables: Dictionary empty ] asGoal.
node := self expectedRBNode_chapter_01_frame_56.
self
assert: aGoal solutions readStream upToEnd equals: { node };
assert: node formattedCode
equals:
'•₀ cons: ((•₁ cdr cons: •₀ car) car cons: (#oats cons: nil)) car
= (•₁ isAtom = (•₂ isAtom cons: •₃ = (•₄ cons: •₂)) isAtom)'.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
That is a good question. We do not know, but we have had fun playing with it so far!
Even Older Games¶
What is this expression obviously equal to?
"TheLittleProverTest, protocol tests"
test_chapter_02_EvenOlderGames_frame_05
| aGoal |
aGoal := [ :rewritten |
[ :ast |
[ :a :c |
ast
acl: [ :prover |
prover focus: [ :o | o ] do: theory ifSameº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :a :c |
a
ifTrue: [ 3 ]
ifFalse: [ c ] ]
contextVariables: Dictionary empty ] asGoal.
self
assert: aGoal solutions readStream upToEnd
equals: { 3 asLiteralRBNode }.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
where
"TheLittleProver, protocol predicates" ifSameº "(dethm cdr/cons (x y) (equal (cdr (cons x y)) y))" ^ [ :x :y | x ifTrue: [ y ] ifFalse: [ y ] ] <~~> [ :x :y | y ]
If TheLittleProver>>#ifSameº can start with an if expression and
end with a variable, then it must also be able to start with a variable and
end with an if expression. So … what else is c equal to, according to
TheLittleProver>>#ifSameº?
"TheLittleProverTest, protocol tests"
test_chapter_02_EvenOlderGames_frame_07
| aGoal node |
aGoal := [ :rewritten |
[ :ast |
[ :a :c |
ast
acl: [ :prover |
prover
focus: [ :o | o ]
do: [ :o :r | theory ifSameº value: r value: o ] ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: Dictionary empty ] ]
asGoalWithUnaryASTof: [ :a :c |
(3 cons: nil) isAtom
ifTrue: [ a ]
ifFalse: [ c ] ]
contextVariables: Dictionary empty ] asGoal.
node := self expectedRBNode_chapter_02_frame_7.
self
assert: aGoal solutions readStream upToEnd equals: { node };
assert: node formattedCode equals: '•₀
ifTrue: [
(3 cons: nil) isAtom
ifTrue: [ •₁ ]
ifFalse: [ •₂ ] ]
ifFalse: [
(3 cons: nil) isAtom
ifTrue: [ •₁ ]
ifFalse: [ •₂ ] ]'.
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
Does the question message a = true tell us anything about the focus nil = nil ifTrue: [ a ] ifFalse: [ b ]?
"TheLittleProverTest, protocol tests"
test_chapter_02_EvenOlderGames_frame_15
| aGoal node |
self skip.
aGoal := [ :rewritten |
[ :ast |
[ :a :b :c |
ast
acl: [ :prover |
prover
focus: [ :o |
(a = true
ifTrue: [
o
ifTrue: [ a ]
ifFalse: [ b ] ]
ifFalse: [ #or = (#black cons: (#coffee cons: nil)) ])
ifTrue: [ c ]
ifFalse: [ c ] ]
do: theory equalSameº.
prover
focus: [ :o |
(a = true
ifTrue: [ o ]
ifFalse: [ #or = (#black cons: (#coffee cons: nil)) ])
ifTrue: [ c ]
ifFalse: [ c ] ]
do: theory ifTrueº.
prover
focus: [ :o |
(a = true
ifTrue: [ o ]
ifFalse: [ #or = (#black cons: (#coffee cons: nil)) ])
ifTrue: [ c ]
ifFalse: [ c ] ]
premise: [ :o |
o
ifTrue: [ c ]
ifFalse: [ c ] ]
do: theory equalIfº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: (Dictionary new
at: #a put: a asRBNode;
at: #b put: b asRBNode;
at: #c put: c asRBNode;
yourself) ] ]
asGoalWithUnaryASTof: [ :a :b :c |
(a = true
ifTrue: [
nil = nil
ifTrue: [ a ]
ifFalse: [ b ] ]
ifFalse: [ #or = (#black cons: (#coffee cons: nil)) ])
ifTrue: [ c ]
ifFalse: [ c ] ]
contextVariables: Dictionary empty ] asGoal.
node := self expectedRBNode_chapter_02_frame_15.
self
assert: (aGoal solutions next: 1) readStream upToEnd
equals: { node };
assert: node formattedCode equals: '(•₀ = true
ifTrue: [ true ]
ifFalse: [ #or = (#black cons: (#coffee cons: nil)) ])
ifTrue: [ •₁ ]
ifFalse: [ •₁ ]'.
^ self exportComputationTreeOfGoal: aGoal limitedTo: 1
where
"TheLittleProver, protocol predicates" ifTrueº "(dethm cdr/cons (x y) (equal (cdr (cons x y)) y))" ^ [ :x :y | true ifTrue: [ x ] ifFalse: [ y ] ] <~~> [ :x :y | x ]
and
"TheLittleProver, protocol predicates" equalIfº ^ [ :a :c :b | [ :d :e | | ancestor dRB | dRB := d asRBNode. ancestor := [ a = b ifTrue: [ d ] ifFalse: [ e ] ] unaryRBNode substituteVariablesUsingDictionary: (Dictionary new at: #a put: a; at: #b put: b; at: #d put: dRB; at: #e put: e asRBNode; yourself). (self unifyº value: ancestor value: c) , ((self unifyº value: a value: dRB) | (self ancestorº value: a value: dRB)) ] asGoal ]
respectively.
Note
"TheLittleProverTest, protocol tests"
test_chapter_02_EvenOlderGames_frame_15_ancestoro
| aGoal |
aGoal := [ :rewritten |
theory ancestorº
value: false asLiteralRBNode
value: rewritten asRBNode ] asGoal.
self
assert:
((aGoal solutions collect: [ :e | e formattedCode ]) next: 25)
readStream upToEnd
equals:
#( 'false car' 'false cdr' '[ false ]' 'false' 'false car car'
'false cdr car' 'false = •₀' '•₀ = false' 'false cons: •₀'
'•₀ cons: false' 'false + •₀' '•₀ + false' 'false - •₀'
'•₀ - false' 'false
ifTrue: [ •₀ ]
ifFalse: [ •₁ ]' '•₀
ifTrue: [ false ]
ifFalse: [ •₁ ]' '•₀
ifTrue: [ •₁ ]
ifFalse: [ false ]' 'false car cdr' 'false cdr cdr' '[ false ] car'
'false car' 'false car car car' 'false cdr car car'
'[ false car ]' '[ false cdr ]' ).
^ self exportComputationTreeOfGoal: aGoal limitedTo: 25
where
"TheLittleProver, protocol predicates" ancestorº ^ MKPredicateBinaryAncestoro
and, in turn,
"MKPredicateBinaryAncestoro, protocol running" goal | g1 g2 | g1 := MKPredicateBinaryParento value: firstArgument value: secondArgument. g2 := [ :p | | pRB | pRB := p asRBNode. (MKPredicateBinaryParento value: pRB value: secondArgument) , (self copy firstArgument: firstArgument; secondArgument: pRB; yourself) ] asGoal. ^ g1 | g2
Moreover, the predicate can be used backwards,
"TheLittleProverTest, protocol tests"
test_chapter_02_EvenOlderGames_frame_15_ancestorobackward
| aGoal |
aGoal := [ :rewritten |
[ :a :b :c |
theory ancestorº
value: rewritten asRBNode
value: ([ :z :x :v |
2 + z
ifTrue: [
x
ifTrue: [ 3 ]
ifFalse: [ 1 ] ]
ifFalse: [ 3 - v ] ]
substituteVariablesUsingSequenceableCollection: {
a asRBNode.
b asRBNode.
c asRBNode }) ] asGoal ] asGoal.
self
assert:
((aGoal solutions collect: [ :e | e formattedCode ]) next: 20)
readStream upToEnd
equals: #( '2 + •₀' '•₀
ifTrue: [ 3 ]
ifFalse: [ 1 ]' '3 - •₀' '2' '◊•₀' '◊•₀' '◊•₀' '◊•₀' '3' '1' '3' '◊•₀'
'◊•₀' '◊•₀' '◊•₀' '◊•₀' '◊•₀' '◊•₀' '◊•₀' '◊•₀' ).
^ self exportComputationTreeOfGoal: aGoal limitedTo: 20
Note
"TheLittleProverTest, protocol tests"
test_chapter_02_EvenOlderGames_frame_15_parento
| aGoal |
aGoal := [ :rewritten |
theory parentº
value: false asLiteralRBNode
value: rewritten asRBNode ] asGoal.
self
assert:
(aGoal solutions collect: [ :e | e formattedCode ]) readStream
upToEnd
equals: #( 'false car' 'false cdr' '[ false ]' 'false' 'false = •₀'
'•₀ = false' 'false cons: •₀' '•₀ cons: false' 'false + •₀'
'•₀ + false' 'false - •₀' '•₀ - false' 'false
ifTrue: [ •₀ ]
ifFalse: [ •₁ ]' '•₀
ifTrue: [ false ]
ifFalse: [ •₁ ]' '•₀
ifTrue: [ •₁ ]
ifFalse: [ false ]' ).
^ self exportComputationTreeOfGoal: aGoal limitedTo: -1
where
"TheLittleProver, protocol predicates" parentº ^ MKPredicateBinaryParento
and, in turn,
"MKPredicateBinaryParento, protocol running" goal | sequenceGoal blockGoal messageNode | sequenceGoal := self unifyº value: secondArgument value: (RBSequenceNode statements: { firstArgument }). messageNode := self unaryMessagesGoal | self binaryMessagesGoal | self ifMessageGoal. blockGoal := self unifyº value: secondArgument value: (RBBlockNode body: (RBSequenceNode statements: { firstArgument })). ^ messageNode | sequenceGoal | blockGoal
Let’s see. Does the if question a car cdr = (#hash cons: (#browns cons:
nil)) tell us anything about the focus a car?
"TheLittleProverTest, protocol tests"
test_chapter_02_EvenOlderGames_frame_57
| aGoal |
self skip.
aGoal := [ :rewritten |
[ :ast |
[ :a |
ast
acl: [ :prover |
prover
focus: [ :o |
a car isAtom
ifTrue: [
a car = a cdr
ifTrue: [ #hominy ]
ifFalse: [ #grits ] ]
ifFalse: [
a car cdr = (#hash cons: (#browns cons: nil))
ifTrue: [ #ketchup cons: o ]
ifFalse: [ #mustard cons: a car ] ] ]
premise: [ :o | o ]
do: [ :o :p :r |
theory consCarCdrº value: r value: p value: o ].
prover
focus: [ :o |
a car isAtom
ifTrue: [
a car = a cdr
ifTrue: [ #hominy ]
ifFalse: [ #grits ] ]
ifFalse: [
a car cdr = (#hash cons: (#browns cons: nil))
ifTrue: [ #ketchup cons: (a car car cons: o) ]
ifFalse: [ #mustard cons: a car ] ] ]
premise: [ :o |
a car isAtom
ifTrue: [
a car = a cdr
ifTrue: [ #hominy ]
ifFalse: [ #grits ] ]
ifFalse: [ o ] ]
do: theory equalIfº ]
then: [ :asts |
theory unifyº value: asts last value: rewritten asRBNode ]
contextVariables: (Dictionary new
at: #a put: a asRBNode;
yourself) ] ]
asGoalWithUnaryASTof: [ :a |
a car isAtom
ifTrue: [
a car = a cdr
ifTrue: [ #hominy ]
ifFalse: [ #grits ] ]
ifFalse: [
a car cdr = (#hash cons: (#browns cons: nil))
ifTrue: [ #ketchup cons: a car ]
ifFalse: [ #mustard cons: a car ] ] ]
contextVariables: Dictionary empty ] asGoal.
self
assert: (aGoal solutions next: 1) readStream upToEnd
equals: { [ :a |
a car isAtom
ifTrue: [
a car = a cdr
ifTrue: [ #hominy ]
ifFalse: [ #grits ] ]
ifFalse: [
a car cdr = (#hash cons: (#browns cons: nil))
ifTrue: [
#ketchup cons:
(a car car cons: (#hash cons: (#browns cons: nil))) ]
ifFalse: [ #mustard cons: a car ] ] ] unaryRBNode }
Note
"TheLittleProverTest, protocol tests"
test_chapter_02_EvenOlderGames_frame_57_premise
| aGoal n a |
aGoal := [ :v :w |
a := RBMessageNode
receiver: (RBLiteralValueNode value: #ketchup)
selector: #cons:
arguments: { (RBMessageNode
receiver: (RBMessageNode
receiver:
(RBMessageNode
receiver: v asRBNode
selector: #car)
selector: #car)
selector: #cons:
arguments: { (RBMessageNode
receiver:
(RBMessageNode
receiver: v asRBNode
selector: #car)
selector: #cdr) }) }.
n := RBMessageNode
receiver:
(RBMessageNode receiver: w asRBNode selector: #car)
selector: #cdr.
(theory unifyº value: n value: a)
| (theory ancestorº value: n value: a) ] asGoal.
self
assert: (aGoal solutions next: 40) readStream upToEnd asString
equals:
'an Array(an Array(•₀ •₀) an Array(RBMessageNode(•₀ car cdr) •₀) an Array(RBMessageNode(•₀ car cdr) •₀) an Array(RBMessageNode(•₀ car cdr car) •₀) an Array(RBMessageNode(•₀ car cdr cdr) •₀) an Array(RBMessageNode(•₀ car cdr car) •₀) an Array(RBMessageNode(•₀ car cdr cdr) •₀) an Array(RBBlockNode([ •₀ car cdr ]) •₀) an Array(RBSequenceNode(•₀ car cdr) •₀) an Array(RBBlockNode([ •₀ car cdr ]) •₀) an Array(RBSequenceNode(•₀ car cdr) •₀) an Array(RBMessageNode(•₀ car cdr car car) •₀) an Array(RBMessageNode(•₀ car cdr cdr car) •₀) an Array(RBMessageNode(•₀ car cdr car car) •₀) an Array(RBMessageNode(•₀ car cdr cdr car) •₀) an Array(RBMessageNode(•₀ car cdr = •₁) •₀) an Array(RBMessageNode(•₀ = •₁ car cdr) •₁) an Array(RBMessageNode(•₀ car cdr cons: •₁) •₀) an Array(RBMessageNode(•₀ cons: •₁ car cdr) •₁) an Array(RBMessageNode(•₀ car cdr + •₁) •₀) an Array(RBMessageNode(•₀ + •₁ car cdr) •₁) an Array(RBMessageNode(•₀ car cdr - •₁) •₀) an Array(RBMessageNode(•₀ - •₁ car cdr) •₁) an Array(RBMessageNode(•₀ car cdr
ifTrue: [ •₁ ]
ifFalse: [ •₂ ]) •₀) an Array(RBMessageNode(•₀
ifTrue: [ •₁ car cdr ]
ifFalse: [ •₂ ]) •₁) an Array(RBMessageNode(•₀
ifTrue: [ •₁ ]
ifFalse: [ •₂ car cdr ]) •₂) an Array(RBMessageNode(•₀ car cdr car cdr) •₀) an Array(RBMessageNode(•₀ car cdr cdr cdr) •₀) an Array(RBMessageNode(•₀ car cdr = •₁) •₀) an Array(RBMessageNode(•₀ = •₁ car cdr) •₁) an Array(RBMessageNode(•₀ car cdr cons: •₁) •₀) an Array(RBMessageNode(•₀ cons: •₁ car cdr) •₁) an Array(RBMessageNode(•₀ car cdr + •₁) •₀) an Array(RBMessageNode(•₀ + •₁ car cdr) •₁) an Array(RBMessageNode(•₀ car cdr - •₁) •₀) an Array(RBMessageNode(•₀ - •₁ car cdr) •₁) an Array(RBMessageNode(•₀ car cdr
ifTrue: [ •₁ ]
ifFalse: [ •₂ ]) •₀) an Array(RBMessageNode(•₀
ifTrue: [ •₁ car cdr ]
ifFalse: [ •₂ ]) •₁) an Array(RBMessageNode(•₀
ifTrue: [ •₁ ]
ifFalse: [ •₂ car cdr ]) •₂) an Array(RBMessageNode(•₀ car cdr car cdr) •₀))'.
^ self exportComputationTreeOfGoal: aGoal limitedTo: 40
