Goals¶

This chapter introduces the basic classes that host the behaviour of the logic system; for the sake of clarity, we proceed in increasing order of complexity, explaining more complex concepts by using simpler ones.

Goal¶

Object subclass: #Goal
	instanceVariableNames: ''
	classVariableNames: ''
	package: 'MicroKanren-Goals'

I and my subclasses represent a small language to construct logical relations. Formally, I adhere to the abstract grammar:

goal        ::=  failed | succeed | binary_goal |
                 fresh | eta | predicate
failed      ::=  "Ø"
succeed     ::=  "✓"
binary_goal ::=  goal (disj | conj | unify | "!" | "≠") goal
disj        ::=  "|º"
conj        ::=  "&º"
unify       ::=  "=º"
fresh       ::=  "fresh" [var] +  "." goal
eta         ::=  "eta" "." goal
var         ::=  "var" Integer
predicate   ::=  functor [value] + "." goal
functor     ::=  String "º"
value       ::=  var | Object

My subclasses have the responsibility to encode combinations of arbitrary goals. In a pure world, they shouldn’t be stateful with respect to a logical computation. In reality, and more important to build visualizations, we will see that some of them keep references to logic objects, variables in particular.

Warning

Although some goals are stateful, their state is related to a computation branch and modified according to the exploration process that looks for substitutions. For any side process that inspects a particular aspect, a copy of the goal has to be made.

To be polymorphic with me, the onState: message has to be implemented, as my subclasses have to; moreover, the reader will understand during the reading of this doc that it is the main message to respond to to drop into a logic computation.

Failed¶

Atomic subclass: #Failed
	instanceVariableNames: ''
	classVariableNames: ''
	package: 'MicroKanren-Goals'

I am a goal that represent logical falsehood, in particular I encode the goalGrammar:failed production. The simpler way to create me is to send the adapting message #asGoal to false, as follows

"GoalTest, protocol tests"
testFailed

   | g |
   g := false asGoal.
   self assert: g solutions equals: #(  ) modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

Succeed¶

Atomic subclass: #Succeed
	instanceVariableNames: ''
	classVariableNames: ''
	package: 'MicroKanren-Goals'

I am a goal that represent logical truth, in particular I encode the goalGrammar:succeed production. The simpler way to create me is to send the adapting message #asGoal to true, as follows

"GoalTest, protocol tests"
testSucceed

   | g |
   g := true asGoal.

   self
      assert: g solutions
      equals: { Var tautology }
      modulo: #asOrderedCollection. " #(#tautology)"

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

where

"Var class, protocol creating"
tautology

   ^ #tautology

Fresh¶

Suspended subclass: #Fresh
	instanceVariableNames: 'variables'
	classVariableNames: ''
	package: 'MicroKanren-Goals'

I am a goal that introduces logic variables, in particular I encode the goalGrammar:fresh production.

"GoalTest, protocol tests"
testFreshFailed

   | g |
   g := [ :q | false asGoal ] asGoal.
   self assert: g solutions equals: #(  ) modulo: #asOrderedCollection. " #()"

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

"GoalTest, protocol tests"
testFreshSucceed

   | g |
   g := [ :q | true asGoal ] asGoal.
   self
      assert: g solutions
      equals: { 0 asReifiedVar }
      modulo: #asOrderedCollection. " an Array(•₀)"

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

where

"Integer, protocol *MicroKanren-core"
asReifiedVar

   ^ self asReifiedWithVarClass: ReifiedVar

and

"Integer, protocol *MicroKanren-core"
asReifiedWithVarClass: aClass

   ^ aClass new
        id: self;
        yourself

"GoalTest, protocol tests"
testFreshMultipleVars

   | g |
   g := [ :q :r | true asGoal ] asGoal.
   self
      assert: g solutions
      equals: (Array with: { 
                0 asReifiedVar.
                1 asReifiedVar })
      modulo: #asOrderedCollection. " an Array(an Array(•₀ •₁))"

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

Moreover, we can also use a block without arguments in order to postpone the computation, for instance to support recursive goals such as

"GoalTest, protocol tests"
testEtaRaw

   | g |
   g := self eternity: Object new.
   self assert: g class equals: Eta

where

"GoalTest, protocol utilities"
eternity: x

   ^ [ self eternity: x ] asGoal

Unify¶

Binary subclass: #Unify
	instanceVariableNames: ''
	classVariableNames: ''
	package: 'MicroKanren-Goals'

I am a goal that represent logical equality, in particular I encode the goalGrammar:unify production.

"GoalTest, protocol tests"
testUnifyThreeWithThree

   | g |
   g := 3 unifyo value: 3.
   self
      assert: g solutions
      equals: { Var tautology }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

_images/GoalTest-testUnifyThreeWithThree.svg

where

"Object, protocol *MicroKanren-core"
unifyo

   ^ [ :anObject | self unifyWith: anObject ]

and

"Object, protocol *MicroKanren-core"
unifyWith: another

   ^ Unify new
        left: self;
        right: another;
        yourself

"GoalTest, protocol tests"
testUnifySymmetryFourWithVar

   | g |
   g := [ :q | 4 unifyo value: q ] asGoal.
   self assert: g solutions equals: { 4 } modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

"GoalTest, protocol tests"
testUnifySymmetryVarWithFour

   | g |
   g := [ :q | q unifyo value: 4 ] asGoal.
   self assert: g solutions equals: { 4 } modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

"GoalTest, protocol tests"
testUnifyWithTopmostSharing

   | g |
   g := [ :r | 
        [ :x :y | r unifyo value: (Array with: x with: y) asCons ]
           asGoal ] asGoal.
   self
      assert: g solutions
      equals: { 
            0 asReifiedVar.
            1 asReifiedVar } asCons
      modulo: #asOrderedCollection. " (•₀ •₁)"

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

"GoalTest, protocol tests"
testUnifyWithTopmostWithoutSharing

   | g |
   g := [ :r | 
        [ :x :y | 
        (LinkedList with: x with: r) asCons unifyo value:
           (LinkedList with: 1 with: y) asCons ] asGoal ] asGoal.
   self
      assert: g solutions
      equals: { 0 asReifiedVar }
      modulo: #asOrderedCollection. " an Array(•₀)"

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

"GoalTest, protocol tests"
testUnifyWithTopmostSharingWithRepetition

   | g |
   g := [ :r | 
        [ :x :y | 
        (LinkedList
            with: x
            with: y
            with: x
            with: y) asCons unifyo value: r ] asGoal ] asGoal.
   self
      assert: g solutions
      equals: { 
            0 asReifiedVar.
            1 asReifiedVar.
            0 asReifiedVar.
            1 asReifiedVar } asCons
      modulo: #asOrderedCollection. " (•₀ •₁ •₀ •₁)"

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

"GoalTest, protocol tests"
testUnifySharing

   | g |
   g := [ :r | 
        [ :x | (r unifyo value: x) , (x unifyo value: true) ] asGoal ]
           asGoal.
   self
      assert: g solutions
      equals: { true }
      modulo: #asOrderedCollection. " #(true)"

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

The previous examples show unifications that can be satisfied; on the contrary, when two objects cannot be equal for any substitution we have a Failed goal holding the counterexample, such as

"GoalTest, protocol tests"
testUnifyFourWithThree

   | g |
   g := 4 unifyo value: 3.
   self assert: g solutions equals: #(  ) modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

Disj¶

Binary subclass: #Disj
	instanceVariableNames: 'combineBlock'
	classVariableNames: ''
	package: 'MicroKanren-Goals'

I am a goal that represent logical union, in particular I encode the goalGrammar:disj production.

On the one hand, false asGoal is the neutral element for disjunction, so that both

"GoalTest, protocol tests"
testDisjFalseFalse

   | g |
   g := false asGoal | false asGoal.
   self assert: g solutions equals: #(  ) modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

and

"GoalTest, protocol tests"
testDisjFalseTrue

   | g |
   g := false asGoal | true asGoal.
   self
      assert: g solutions
      equals: { Var tautology }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

behave as usual in logic. On the other hand,

"GoalTest, protocol tests"
testDisjTrueTrue

   | g |
   g := true asGoal | true asGoal.
   self
      assert: g solutions
      equals: { 
            Var tautology.
            Var tautology }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

surprises with two solutions instead of one because true asGoal |º b doesn’t bypass the exploration of the goal b. For the sake of clarity, two solutions are provided both by

"GoalTest, protocol tests"
testDisjThreeWithVarOrThreeWithVar

   | g |
   g := [ :a | (3 unifyo value: a) | (3 unifyo value: a) ] asGoal.
   self
      assert: g solutions
      equals: { 3. 3 }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

and

"GoalTest, protocol tests"
testDisjThreeWithThreeOrFourWithVar

   | g |
   g := [ :a | (3 unifyo value: 3) | (4 unifyo value: a) ] asGoal.
   self
      assert: g solutions
      equals: { 
            0 asReifiedVar.
            4 }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

which leaves the variable unbound in the leftmost path. Disjunction is commutative, so that both

"GoalTest, protocol tests"
testDisjThreeWithVarOrFourWithVar

   | g |
   g := [ :a | (3 unifyo value: a) | (4 unifyo value: a) ] asGoal.
   self
      assert: g solutions
      equals: { 3. 4 }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

and

"GoalTest, protocol tests"
testDisjFourWithVarOrThreeWithVar

   | g |
   g := [ :a | (4 unifyo value: a) | (3 unifyo value: a) ] asGoal.
   self
      assert: g solutions
      equals: { 4. 3 }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

are satisfied by the same set of substitutions or, in other words, have the same paths connecting the leaves to the roots. Disjunction is associative, so that both trees

"GoalTest, protocol tests"
testDisjThreeFourThenFive

   | g |
   g := [ :a | 
        (3 unifyo value: a) | (4 unifyo value: a) | (5 unifyo value: a) ]
           asGoal.
   self
      assert: g solutions
      equals: { 3. 5. 4 }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

and

"GoalTest, protocol tests"
testDisjThreeThenFourFive

   | g |
   g := [ :a | 
        (3 unifyo value: a)
        | ((4 unifyo value: a) | (5 unifyo value: a)) ] asGoal.
   self
      assert: g solutions
      equals: { 3. 4. 5 }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

have the same set of leaves but different branching structures.

Conj¶

Binary subclass: #Conj
	instanceVariableNames: ''
	classVariableNames: ''
	package: 'MicroKanren-Goals'

I am a goal that represent logical intersection, in particular I encode the goalGrammar:conj production.

On the one hand, true asGoal is the neutral element for disjunction, so that both

"GoalTest, protocol tests"
testConjTrueTrue

   | g |
   g := true asGoal , true asGoal.
   self
      assert: g solutions
      equals: { Var tautology }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

and

"GoalTest, protocol tests"
testConjTrueThreeWithThree

   | g |
   g := [ :q | true asGoal , (3 unifyo value: 3) ] asGoal.
   self
      assert: g solutions
      equals: { 0 asReifiedVar }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

are succeeding goals. On the other hand, false asGoal makes a conjunction false asGoal &º b failing for any goal b, as in

"GoalTest, protocol tests"
testConjFalseThreeWithVar

   | g |
   g := [ :q | false asGoal , (3 unifyo value: q) ] asGoal.
   self assert: g solutions isEmpty.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

Conjunctions essentially propagates unified values by the left hand side subgoal into the right hand side one; for the sake of clarity, the following examples attempts to unify the same variable with two different values yielding no solution (but providing the corresponding counterexample)

"GoalTest, protocol tests"
testConjThreeFour

   | g |
   g := [ :a | (3 unifyo value: a) , (4 unifyo value: a) ] asGoal.
   self assert: g solutions isEmpty.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

while the following one succeeds and also shows the commutativity of the operator

"GoalTest, protocol tests"
testConjSymmetry

   | g |
   g := [ :a | (a unifyo value: 4) , (4 unifyo value: a) ] asGoal.
   self assert: g solutions equals: { 4 } modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

In the same spirit, the following examples shows two succeeding conjunctions, the former introduces a variable in a nested goal,

"GoalTest, protocol tests"
testConjThreeFresh

   | g |
   g := [ :a | (3 unifyo value: a) , [ :b | 4 unifyo value: b ] asGoal ]
           asGoal.
   self assert: g solutions equals: { 3 } modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

the latter, introduces both variables in the topmost goal

"GoalTest, protocol tests"
testConjThreeFourWithTwoVars

   | g |
   g := [ :a :b | (3 unifyo value: a) , (4 unifyo value: b) ] asGoal.
   self
      assert: g solutions
      equals: { { 3. 4 } }
      modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

Sharing among variables can be shown with both a succeeding example

"GoalTest, protocol tests"
testConjSucceedingSharing

   | g |
   g := [ :z | 
        [ :x | (3 unifyo value: x) , (z unifyo value: x) ] asGoal ]
           asGoal.
   self assert: g solutions equals: #( 3 ) modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

and a failing one

"GoalTest, protocol tests"
testConjFailingSharing

   | g |
   g := [ :x :y :z | 
        (3 unifyo value: x) , (z unifyo value: x) , (z unifyo value: 4) ]
           asGoal.
   self assert: g solutions equals: #(  ) modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

Finally, the combination of a failing conjunction with a succeeding disjunction produces the following computation

"GoalTest, protocol tests"
testConjDisj

   | g |
   g := [ :a | 
        (3 unifyo value: a) , (4 unifyo value: a) | (a unifyo value: 0) ]
           asGoal.
   self assert: g solutions equals: { 0 } modulo: #asOrderedCollection.

   ^ self exportComputationTreeOfGoal: g limitedTo: -1

µkanrenst

Navigation

Related Topics

Goals¶

Goal¶

Failed¶

Succeed¶

Fresh¶

Unify¶

Disj¶

Conj¶