-
Notifications
You must be signed in to change notification settings - Fork 16
Home
This tutorial assumes zero experience with Logic Programming, but some experience with Clojure.
Please direct any feedback to Ambrose Bonnaire-Sergeant via http://twitter.com/#!/ambrosebs or abonnairesergeant@gmail.com
Many thanks to these Clojurists for their invaluable feedback and encouragement!
David Nolen Twitter, Github, Blog
Jim Duey Twitter
This tutorial is meant to be used with a Clojure REPL handy. An example project has been set up.
Clone with:
git clone git@github.com:frenchy64/Logic-Starter.git
You should be able to run all code examples in the logic-introduction.core namespace.
If any code examples appear to be missing pairs of square braces, please check the wiki source and separate each brace with a space (ie. [ [ and ] ]). If you know how to escape this character sequence in a code block with Markdown, please let me know.
Welcome!
In the following sections, we will explore an implementation of miniKanren, a logic programming system.
At least two ports of miniKanren to Clojure have been made:
This tutorial will use core.logics implementation, which resides in the namespace clojure.core.logic.minikanren. core.logics port is rather faithful to miniKanren, which has its roots in Scheme.
Because of this, it carries some historical baggage.
Function names are rather terse compared to idiomatic Clojure, but we will try and help by providing some mnemonics. But don't worry, a little practice and they'll be like old friends.
We also follow the convention of naming relations with the suffix "o".
This tutorial will explore some basic logic programming concepts, and is intended as motivation for more involved texts, such as The Reasoned Schemer.
Enjoy playing with the type checker, but keep an eye on it ... I think I saw it move!
Let's say we want to check the resulting type for this expression:
(let [f (fn [a] a)
g 1]
(f g))We propose an interface for a type checker:
(typed
<environment>
<expression>
<expected-type>)
;=> <boolean>An initial version of typed (aka. "Type Determine") takes three arguments:
- an environment (map of variables to values),
- an expression,
- and an expected resulting type.
typed returns true if the resulting type of executing the expression in the given environment is equal to the third argument.
In other words, return true if it type-checks successfully.
Here are some imaginary executions of typed.
(typed
[f (fn [a] a)
g 1]
(f g)
Integer)
;=> true
(typed
[f (fn [a] a)
g 1]
(f g)
Float)
;=> falseLogic Programming Concept: Relations
A relation is simply a function that returns a goal as its value.
Logic Programming Concept: Goals
A goal can either succeed or fail.
All relations return goals.
There are two special goals that are used like constants:
clojure.core.logic.minikanren/succeedrepresents the successful goalclojure.core.logic.minikanren/failrepresents a failed goal.We will see examples of using these two goals throughout the tutorial.
Let's propose a new interface for typed that converts it into a relation.
(typedo
<environment>
<expression>
<expected-type>)
;=> <goal>By convention, relations end their name with "o".
Compare to typeds calling interface:
(typed
<environment>
<expression>
<expected-type>)
;=> <boolean>Note what we changed:
- We renamed
typedtotypedo -
typedoreturns a goal instead of a Boolean value
Logic Programming Concept: run
To execute a logic expression, we use
run*.
run*is not a relation; it does not return goal.
As an example, let's roughly translate the following code,
(let [f (fn [a] a)
g 1]
(f g))into our type checker, and test that it returns an integer.
(run* [q]
(typedo [ ['f :- [Integer :> Integer] ] ;; 'f is of type Integer -> Integer
['g :- Integer] ;; 'g is of type Integer
]
[:apply 'f 'g] ;; Determine the resulting type of ('f 'g) ..
Integer) ;; and succeed if it is Integer
)
;=> (_.0)Here are some facts:
-
:-is pronounced "is of type". -
[Integer :> Integer]represents the type of a function that take a single argument of typeIntegerand returns a value of typeInteger. -
['f :- [Integer :> Integer] ]is called a type association. -
[ ['f :- [Integer :> Integer] ] ['g :- Integer] ]is an environment (represented by a vector of type associations). -
[:apply x y]represents the function call(x y).
There are still mysteries about run* that we will leave for now:
- What does
run*s first argument,[q], mean? - What exactly is
run*s return value? We've already said it's not a relation, therefore it doesn't return a goal, but what is it?
Let's get a feel for our type checker.
(run* [q]
(typedo [ ['f :- [Float :> Integer] ]
['g :- Integer]
]
[:apply 'f 'g]
Integer)
)
;=> ()The run returns () because typedo fails.
typedofails because it returns an unsuccessful goal.
Expanded, the run is equivalent to
(run* [q]
fail
)Why did typedo fail?
(run* [q]
(typedo [ ['f :- [Float :> Integer] ]
['g :- Float]
]
[:apply 'f 'g]
Integer)
)
;=> (_.0)The run returns a non-empty list because no goals failed.
typedosucceeds because it returns a successful goal.
Expanded, the run is equivalent to
(run* [q]
succeed
)Why did typedo succeed?
(run* [q]
(typedo [ ['f :- [Float :> Integer] ]
['g :- Float]
['h :- [Integer :> Float] ]
]
[:apply 'h [:apply 'f 'g] ]
Float)
)
;=> (_.0)The run returns a non-empty list because no goals failed. (Why does typedo succeed?)
(run* [q]
(typedo [ ['max :- [Integer :> [Integer :> Integer] ]]
['a :- Integer]
['b :- Integer]
]
[:apply [:apply 'max 'a] 'b]
Integer)
)
;=> (_.0)The run returns a non-empty list because no goals failed. (Why does typedo succeed? What does 'max probably do?)
(run* [q]
(typedo [ ['and :- [Boolean :> [Boolean :> Boolean] ]]
['x :- Boolean]
['y :- Boolean]
]
[:apply [:apply 'and 'x] 'y]
Boolean)
)
;=> (_.0)The run returns a non-empty list because no goals failed. (Why does typedo succeed? What does 'and probably do?)
Does our type checker support polymorphism?
(run* [q]
(typedo [ ['int :- [Number :> Integer] ]
['x :- Double]
]
[:apply 'int 'x]
Integer)
)
;=> ()The run returns () because typedo returns a failed goal.
Why does typedo fail?
Where does typedo fail?
Hint: (= true (isa? Double Number))
(run* [q]
(typedo [ ['int :- [Double :> Integer] ]
['x :- Double]
]
[:apply 'int 'x]
Integer)
(typedo [ ['int :- [Float :> Integer] ]
['x :- Float]
]
[:apply 'int 'x]
Integer)
(typedo [ ['int :- [Integer :> Integer] ]
['x :- Integer]
]
[:apply 'int 'x]
Integer)
)
;=> (_.0)The run returns a non-empty list because no goals failed.
In what situations does run* return an empty list?
In what situations does run* return a non-empty list?
A logic variable is a lexically scoped variable that can be assigned to exactly once after it is "fresh".
A fresh variable is conceptually similar to a declared variable that has no useful value.
run*s first argument is a vector containing a name. The name is declared as a fresh logic variable.
run* returns a list of values assigned to q if no goals in the run fail.
(run* [q])
;=> (_.0)A fresh variable is printed with a non-negative number prefixed by "_.".
In logic programming, assignment and equality tests are performed by unification.
Unification is represented by the macro clojure.core.logic.minikanren/==, and
is pronounced "unify".
Unify is
==for historical reasons, being faithful to the Scheme implementation of miniKanren. Don't confuse it withclojure.core/==
== is a relation; it returns an successful goal if unification is successful, otherwise
an unsuccessful goal.
(run* [q]
(== 1 1))
;=> (_.0)1 is the same as 1, so unification succeeds.
The run returns a non-empty list of the values of q because no goals failed.
Because q is fresh, (_.0) is returned.
(run* [q]
(== 0 1))
;=> ()0 is not same as 1, so unification fails.
The run returns () because a goal failed. (Which goal failed?)
The Law of Fresh
If
xis fresh, then (== v x) succeeds and associatesxwithv. (The Reasoned Schemer)
(run* [q]
(== q 1))
;=> (1)As q is fresh, it is associated with 1, and the expression succeeds.
No goals fail, and q is 1, so the expression returns (1)
(run* [q]
(== 1 q)
(== q 1))
;=> (1)As q is fresh, it is associated with 1, and the first unification succeeds.
Order does not matter with unification. (== q 1) is identical to (== 1 q)
As q is 1, which is the same as 1, the second unification succeeds.
No goals fail, so the expression returns (1).
(run* [q]
(== q 1)
(== q 2))
;=> ()As q is fresh, it is associated with 1, and the first unification succeeds.
q (which is now associated with 1) is not the same as 2, so the second unification fails.
A goal fails, so the expression returns ()
(run* [q]
(typedo [ ['int :- [Double :> Integer] ]
['x :- Integer]
]
[:apply 'int 'x]
Integer)
(== q true))
;=> ()Why does this run return ()?
(run* [q]
(typedo [ ['int :- [Double :> Integer] ]
['x :- Double]
]
[:apply 'int 'x]
Integer)
(== q true))
;=> (true)Why does this run return (true)?
Why does this run return (java.lang.Integer)?
(run* [q]
(typedo [ ['int :- [Integer :> q] ]
['x :- Integer]
]
[:apply 'int 'x]
Integer))
;=> (java.lang.Integer)Because typedo would succeed if q was associated with java.lang.Integer. (Why?)
Why does this run return (java.lang.Integer)?
(run* [q]
(typedo [ ['int :- [Integer :> Integer] ]
['x :- q]
]
[:apply 'int 'x]
Integer))
;=> (java.lang.Integer)Because typedo would succeed if q was associated with java.lang.Integer. (Why?)
Why does this run return ([java.lang.Integer :> java.lang.Integer])?
(run* [q]
(typedo [ ['int :- q]
['x :- Integer]
]
[:apply 'int 'x]
Integer))
;=> ([java.lang.Integer :> java.lang.Integer])Because typedo would succeed if q was associated with [java.lang.Integer :> java.lang.Integer]. (Why?)
Why does this run return ()?
(run* [q]
(typedo [ ['int :- [Integer :> Double] ]
['x :- q]
]
[:apply 'int 'x]
q))
;=> ()Because no values can be associated with q such that typedo succeeds. (Why?)
Logic Programming Concept: fresh
freshtakes a vector of names which are initialized to fresh logic variables.
When one variable is associated with another, we say they co-refer, or share. (The Reasoned Schemer, pg 9)
(run* [q]
(fresh [a]
(== q a)
(== a 1)))
;=> (1)Both q and a are fresh when they are associated with each other. q gets whatever
associations a gets.
a is associated with 1, which is q.
No goals fail, so the expression returns (1).
Why does this expression return ( [java.lang.Double java.lang.Integer] )?
(run* [q]
(fresh [a b]
(typedo [ ['int :- [Integer :> Double] ]
['x :- b]
]
[:apply 'int 'x]
a)
(== q [a b])))
;=> ([java.lang.Double java.lang.Integer])Because typedo would succeed if both a was associated with java.lang.Double and b was associated with java.lang.Integer. (Why?)
Why does this expression return ([ [_.0 :> java.lang.Integer] _.0])?
(run* [q]
(fresh [a b]
(typedo [ ['int :- a]
['x :- b]
]
[:apply 'int 'x]
Integer)
(== q [a b])))
;=> ([ [_.0 :> java.lang.Integer] _.0])Because typedo would succeed if a was associated with [_.0 :> java.lang.Integer] and b was associated with _.0.
_.0 represents a fresh variable. The typedo would succeed if all instances of _.0 are substituted with the same (arbitrary) type.
Verify this by substituting all _.0s with a type.
Why does this expression return ( [ [_.0 :> _.1] _.0 _.1] )?
(run* [q]
(fresh [a b c]
(typedo [ ['int :- a]
['x :- b]
]
[:apply 'int 'x]
c)
(== q [a b c])))
;=> ([ [_.0 :> _.1] _.0 _.1])Because typedo would succeed if
-
awas associated with[_.0 :> _.1]and -
bwas associated with_.0and -
cwas associated with_.1.
The typedo would succeed
- if all instances of
_.0are substituted with the same (arbitrary) type and - if all instances of
_.1are substituted with the same (arbitrary) type.
Verify this by substituting all _.0s with a type and substituting all _.1s with a type.
Why does the following expression not yield a value?
(run* [q]
(fresh [a x]
(typedo [ ['f :- [Integer :> a] ]
['g :- Integer] ]
x
Float)
(== [x a] q)))
;Because there are infinite values of q that satisfy typedo.
Why does the following expression yield a value?
(run 2 [q]
(fresh [a x]
(typedo [ ['f :- [Integer :> a] ]
['g :- Integer] ]
x
Float)
(== [x a] q)))
;=> ([ [:apply f g] java.lang.Float]
; [ [:apply [:apply f g] g] [java.lang.Integer :> java.lang.Float] ])Because we requested for 2 values of q that satisfy typedo.
Verify each combination satisfies typedo.
Why does the following expression yield a value?
(run 4 [q]
(fresh [a x]
(typedo [ ['f :- [Integer :> a] ]
['g :- Integer] ]
x
Float)
(== [x a] q)))
;=> ([ [:apply f g] java.lang.Float]
; [ [:apply [:apply f g] g] [java.lang.Integer :> java.lang.Float] ]
; [ [:apply [:apply [:apply f g] g] g] [java.lang.Integer :> [java.lang.Integer :> java.lang.Float] ]]
; [ [:apply [:apply [:apply [:apply f g] g] g] g] [java.lang.Integer :> [java.lang.Integer :> [java.lang.Integer :> java.lang.Float] ]] ]) Because we requested for 4 values of q that satisfy typedo.
The macro
conderesides at `clojure.core.logic.minikanren/conde
Why does this expression return nil?
(cond
false true)
;=> nilBecause the question is falsy, cond falls though and returns nil.
Why does this expression fail?
(run* [q]
(conde
(fail succeed)))
;=> ()Because the question fails, conde falls through and fails.
Why does this expression return true?
(cond
true true)
;=> trueBecause the question is truthy, and the answer is true.
Why does this expression succeed?
(run* [q]
(conde
(succeed succeed)))
;=> (_.0)Because the question succeeds, and the answer is successful.
condeclauses have 1 question and 0 or more answers.
Why does this expression succeed?
(run* [q]
(conde
(succeed succeed succeed)
(succeed fail)
(succeed succeed)))
;=> (_.0 _.0)The first clause succeeds because the question and the answers succeed.
q is still fresh.
q is refreshed to a new fresh value.
The second clause fails because the answer fails.
q is refreshed to a new fresh value.
The third clause succeeds because the question and the answers succeed.
q is still fresh.
At least one clause succeeds, so conde succeeds.
Two fresh values are returned, one from each successful clause.
Why does this expression succeed?
(run* [q]
(conde
((== 'olive q) succeed)
((== 'oil q) succeed)))
;=> (olive oil)Because (== 'olive q) succeeds, and therefore the answer is succeed.
The succeed preserves the association of q to 'olive.
To get the second value we "pretend" that (== 'olive q) fails; this
imagined failure "refreshes" q.
Then (== 'oil q) succeeds.
The succeed preserves the association of q to 'oil.
We then pretend that (== 'oil q) fails, which once again refreshes q.
Since no more goals succeed, we are done.
(The Reasoned Schemer, Pg 11)
Since at least one conde clause succeeded, the conde expression succeeds.
Since no goals fail, the expression succeeds.
The Law of conde
To get more values from conde, pretend that the successful conde line has failed, refreshing all variables that got an association from that line.
(The Reasoned Schemer)
The "e" in conde stands for "every line", since every line can succeed.
(The Reasoned Schemer, Pg 12)
Why isn't the value of this expression (olive oil)?
(run 1 [q]
(conde
((== 'olive q) succeed)
((== 'oil q) succeed)))
;=> (olive)Because (== 'olive q) succeeds and because run 1 produces at most one value of q.
(The Reasoned Schemer, pg 12)
Experiment with the number of clauses and with varying the number of output values.
Why is the value of this expression (extra virgin)?
(run 2 [q]
(conde
((== 'extra q) succeed)
((== 'virgin q) succeed)
((== 'olive q) succeed)
((== 'oil q) succeed)))
;=> (extra virgin)Because run 2 produces at most two values.
Why is the value of this expression (extra virgin olive oil)?
(run* [q]
(conde
((== 'extra q) succeed)
((== 'virgin q) succeed)
((== 'olive q) succeed)
((== 'oil q) succeed)))
;=> (extra virgin olive oil)Because all clauses succeed and because run* keeps producing values until
they are exhausted.
matche is a syntactic variation on conde that introduces pattern matching.
The following expressions are equivalent.
(run* [q]
(conde
((== 'extra q) succeed)
((== 'virgin q) succeed)
((== 'olive q) succeed)
((== 'oil q) succeed)))
;=> (extra virgin olive oil)(run* [q]
(matche [q]
(['extra] succeed)
(['virgin] succeed)
(['olive] succeed)
(['oil] succeed)))
;=> (extra virgin olive oil)matche supports wildcards with _.
(run* [q]
(fresh [a o]
(== a [1 2 3 4 5])
(matche [a]
([_]
(== q "first"))
([ [1 2 3 4 5] ]
(== q "second"))
(["a"]
(== q "third")))))
;=> ("first" "second")The first clause matches because the wildcard matches [1 2 3 4 5].
The second clause matches because (== [1 2 3 4 5] [1 2 3 4 5] ) succeeds.
The third clause fails because (== [1 2 3 4 5] "a") fails.
matche supports destructuring with ..
(run* [q]
(fresh [a o]
(== a [1 2 3 4 5])
(matche [a]
([ [1 2 . [3 4 5] ]]
(== q "first"))
([ [1 2 3 . [4 5] ]]
(== q "second"))
([ [1 . _] ]
(== q "third")))))
;=> ("first"
; "second"
; "third")The first clause matches because [1 2 . [3 4 5] ] matches [1 2 3 4 5]
The second clause matches because [1 2 3 . [4 5] ] matches [1 2 3 4 5]
The third clause matches because [1 . _] matches [1 2 3 4 5] when the wildcard is replaced with [2 3 4 5]
Wildcards match the minimum possible amount to satisfy matching.
(run* [q]
(fresh [a o]
(== a [1 2 3 4 5])
(matche [a]
([ [1 . _] ]
(== q "first"))
([ [_ . o] ]
(== q ["second" o])))))
;=> ("first"
; ["second" (2 3 4 5)])The _ in the second clause is guaranteed just to match 1, as that is
the absolute minimum required to satisfy matching.
matche implicitly declares variables prefixed by "?".
(run* [q]
(fresh [a o]
(== a [1 2 3 4 5])
(matche [a]
([ [1 . o] ]
(== q ["one" o]))
([ [1 2 . ?o] ]
(== q ["two" ?o]))
([ [o . ?o] ]
(== q ["third" o ?o])))))
;=> (["one" (2 3 4 5)]
; ["two" (3 4 5)]
; ["third" 1 (2 3 4 5)] matche declares ?o for us, and ?o acts like any other variable.
Before we go on to more advanced uses of typedo let's explore a utility function it uses, geto.
(ns logic-introduction.core
(:refer-clojure :exclude [inc reify ==])
(:use [clojure.core.logic minikanren prelude nonrel match disequality]))
(defn geto [key env value]
"Succeed if type association [key :- value] is found in vector env."
(matche [env]
([ [[key :- value] . _] ])
([ [_ . ?rest] ] (geto key ?rest value))))Here are some sample executions of geto
(run* [q]
(geto 'f
[ ['f :- Integer] ]
Integer)
(== q true))
;=> (true)The type association ['f :- Integer] occurs in the environment [ ['f :- Integer] ], so geto succeeds.
(run* [q]
(geto 'g
[ ['f :- Integer] ]
Integer)
(== q true))
;=> ()The type association ['g :- Integer] does not occur in the environment [ ['f :- Integer] ], so geto fails.
(run* [q]
(geto 'c
[ ['f :- [Integer :- Float] ]
['a :- Integer]
['b :- Integer]
['c :- Integer]
['d :- Integer] ]
Integer)
(== q true))
;=> (true)The type association ['c :- Integer] occurs in the environment given, so geto succeeds.
__
Can geto do anything else interesting?
What is a in the following expression?
(run* [q]
(fresh [a]
(geto 'c
[a]
Integer)
(== q a)))
;=> ([c :- java.lang.Integer])a is the type association needed to satisfy geto.
What is a in the following expression?
(run* [q]
(fresh [a]
(geto 'a
[ ['f :- [Integer :- Float] ]
a
['b :- Integer]
['c :- Integer]
['d :- Integer] ]
Integer)
(== q a)))
;=> ([a :- java.lang.Integer])a is the type association needed to satisfy geto.
What is interesting about the following expression?
(run* [q]
(fresh [a]
(geto 'c
[ ['f :- [Integer :- Float] ]
a
['b :- Integer]
['c :- Integer]
['d :- Integer] ]
Integer)
(== q a)))
;=> ([c :- java.lang.Integer] _.0)It returns two values of a satisfying geto.
The first value, [c :- java.lang.Integer], gets associated on the 2nd line of the environment, similar to the previous example.
This satisfies geto, so a successfully gets associated a value.
It looks like a is then made fresh, and the rest of environment is searched.
Then the 4th line of the environment satisfies geto, because it is ['c :- Integer].
This satisfies geto, so a successfully gets a value, that happens to be fresh.
What does the result of this expression tell us?
(run* [q]
(fresh [a b c d]
(geto 'c
[a b c d]
Integer)
(== q [a b c d])))
;=> ([ [c :- java.lang.Integer] _.0 _.1 _.2]
; [_.0 [c :- java.lang.Integer] _.1 _.2]
; [_.0 _.1 [c :- java.lang.Integer] _.2]
; [_.0 _.1 _.2 [c :- java.lang.Integer] ])The result tells us that geto always searches to the end of the environment vector, collecting results along the way,
regardless of whether it found a match previously.
This seems inefficient.
Advanced, non-relational variants of
condeallow control over how many clauses are executed, trimming results for increased efficiency. This comes at the cost of flexibility, so they should be used carefully. (seecondaandcondein The Reasoned Schemer)
Explain the following expression, and its result:
(run 6 [q]
(fresh [a]
(geto 'c
a
Integer)
(== q a)))
;=> (([c :- java.lang.Integer] . _.0)
; (_.0 [c :- java.lang.Integer] . _.1)
; (_.0 _.1 [c :- java.lang.Integer] . _.2)
; (_.0 _.1 _.2 [c :- java.lang.Integer] . _.3)
; (_.0 _.1 _.2 _.3 [c :- java.lang.Integer] . _.4)
; (_.0 _.1 _.2 _.3 _.4 [c :- java.lang.Integer] . _.5))What does the list destructuring, and the fresh variable and the end of every result mean?
What does _.0 represent in the first item of the result?
Disequality constraints guarantee that two terms can never become equal. It is comparable to the inverse of unification.
!= is used to describe this relationship.
This expression succeeds
(run* [q]
(!= q 2)
(== q 1))
;=> (1)because (!= q 2) guarantees q not to be associated with 2.
(== q 1) assigns q to 1 successfully.
This expression fails
(run* [q]
(!= q 2)
(== q 2))
;=> ()because (!= q 2) guarantees q not to be associated with 2.
The disequality constraint causes (== q 2) to fail.
Therefore the run yields ().