[:toc:]
Logic: Programming it is about. - Relational Programming :-)
-
reify: to convert mentally into a thing; to materialize.
-
unify: to make, form into, or cause to become one; to combine (two or more) in one; to join (one or more) to or with another or others so as to form one whole or unit; to unite, consolidate.
-
expression The action of expressing or representing (a meaning, thought, state of things) in words or symbols; the utterance (of feelings, intentions, etc.). The action or process of manifesting (qualities or feelings) by action, appearance or other evidences or tokens.
A logical statement is built along states from variables, and goals.
Create an initial state, then obtain some variables (and resulting state) from it.
Construct a goal consisting of variable bindings and logical operations (AND, OR), or predicates.
Then evaluate the goal using the state resulting from making the variables.
Evaluating a goal returns all possible solutions to the statement in the form of a number of states containing suitable variable bindings.
Note: Most often, the EmptyState is used as initial state.
A predicate is what -given some variable- evaluates to #t or #f (with/in a given state).
Any value used in a state must be unifiable.
Unifying two values produces zero or more possible states, where variables that may be contained in the values may be bound in various combinations.
Basic constructs of relational programming are
- the Goals
Yeahaka#s(akaSucceed) andFailaka#u,
- fresh logic Variables
,u,v,w... - operators
==, akaEq,FreshandConde.
The laws of operators fresh, == and conde are postulated:
(== v w) is the same as (== w v)
If x is fresh, then (== v x) succeeds and associates x with v.
To get more values from conde, pretend that the successful line has failed, refreshing all variables that got an association from that line.
The entire system is comprised of a handful of facilities and functions for
- the implementation of variables,
- streams themselves,
- the interface for creating and combining streams, and
- four primitive goal constructors.
A logical Variable may be named or anonymous.
- Method
Fresh(name string) Vcreates a named Variable - Method
V() Vproduces a new anonymous Variable
Note: Internally, V() calls Fresh with a auto-generated (and previously unused) name-string.
Equality is determined by coincidence of their name-string.
u.Equal(v) boolreports it.
In our context. this is what a Variable may represent, what a Variable may be bound to.
- Some call it Value - as in "Value of a Variable".
- Some call it Term - as in "Term as part of an eXpression".
Some eXpression x may be very basic, e.g consist of just one single thing (Atom).
And such, in turn, may just happen to be a Variable.
x.IsVariable() boolreports this,x.AsVariable() (V, bool)reveals the Variable (if any)v.Expr() Xexpresses a Variablevas eXpression.
Thus, we have a circular self reference:
- any Variable may camouflage as an eXpression, and
- some eXpression may reveal to be nothing but a single Variable.
V->X->V->X->V->X->V->X->V->X->V->X->V->X->V->X->V ...
This (indirect) self-reference is almost magical - and very important.
In the literature we meet a lot of overloaded terminology here and we need to take great care in order to avoid confusion.
Constraint programming calls it: Assignment or assignation (or model).
How to bind a Variable and/with/to some eXpression?
A bind consists of:
- some Variable being bound, and
- some eXpression(Value/Term) related to it, given to it, assigned to it.
The eXpression(Value/Term) substitutes the Variable, so to say.
Thus: bind establishes a relation between V and X.
Within the notation of symbolic expressions we may write individual members of such relation as pair: (x . y) or (y . 5) or (x . (y . 5)).
The Binding of some Variable may change over time.
Any Variable may be (or may become) unbound.
No Variable can ever be bound to more than one eXpression at the same time.
Note: Some bound eXpression may itself be a logic Variable: e.g. (y . 5)(x . y)
Once there is a bind, we may use it on any other eXpression (think: formula).
Every occurrence of the Variable (being bound) shall be replaced/substituted by the eXpression (the Variable is bound to/with).
Thus, we may need to Walk the eXpression, and replace any occurrence of the Variable.
b.Bind( V, X )
b.Bound( V ) -> ( value X, isBound bool )
b.IsBound( V ) -> ( isBound bool )
b.Resolve( X ) -> X
b.Walk( X ) -> X
b.Occurs( V, X ) -> bool
b.Unify(x, y X ) -> bool - triangular
- idempotent
Mainly, it's just a bind.Ings. (Which some call Substitution).
Thus, a logical state is a collection of variable bindings.
Some say: A _Substitution_ `S` is a mapping/association between logic variables `V` and their values `T` (also called `terms`).
Note: Some `T` may itself be a logic Variable: e.g. `(y . 5)(x . y)`
() is the _empty Substitution_
b.Unify(a, b) attempts to unify a and b (with respect to binding b) and
returns a (potentially extended) Substitution, or #f (fails).
Any eXpression containing some logic variable may be considered "vague" due to their "real" or "appropriate" or "right" content / meaning / value not being known (yet).
In general, "Reify" means to convert mentally into a thing; to materialize it. In our context,Reification is the process of turning some eXpression into another eXpression that does not contain any logic variable any more.
S.Reify( X ) -> XReify takes an arbitrary eXpression, perhaps containing variables, and returns it reified.
Goals are used to specify logical statements.
A Goal g is a function that maps a substitution s to an ordered sequence of zero or more values.
(These values are almost always substitutions.)
The sequence of values may be infinite. Thus, it is not a list but as a special kind of stream.
type Goal func(S) ValueStream:Evaluate a Goal to produce zero or more States, or collections of variable bindings/Substitutions.
(mZero) represents the empty stream of values.
(Unit a) represents the stream containing just a, if a is a value.
(Choice a f) represents a non-empty stream, where
- a is the first value in the stream, and where
- f is a function of zero arguments. Invoking the function f produces the remainder of the stream.
type Cons struct {head, tail}is an alternative name & implementation for Choice
A Goal does either
- fail, or
- succeed
Evaluating a Fail goal always results in zero states.
Evaluating a UnifyVal goal attempts to unify a variable and a value.
Evaluating a UnifyVar goal attempts to unify the variables.
A Conjunction goal evaluates its sub-goal a using a given state, then evaluates sub-goal b using the results.
Evaluating a Disjunction goal returns all the possible states of evaluating a and b.
Evaluating a Predicate goal returns the given state only if the function returns true.
αKanren extends core miniKanren with operators for nominal logic programming
introduces noms ("Names" / "Atoms")
used to limit the scope of a nom within a term ...
A term constructed using tie ◃▹ is called binder. In the term created by the expression
(◃▹ a t), all occurrences of the nom a within term t are considered bound.
We refer to the term t as the body of (◃▹ a t), and to the nom a as being in binding position.
The ◃▹ constructor does not create noms; rather, it delimits the scope of noms, already introduced using fresh.
./.
miniKanren - a canonical implementation.
Implements the language described in the paper:
William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl). To appear in the Proceedings of the 2012 Workshop on Scheme and Functional Programming, Copenhagen, Denmark, 2012.
Core µKanren: ==(aka Unify), fresh, conde
Extensions: =/=, symbolo, numbero, absento
µKanren - a reference implementation.
The little Schemer The seasoned Schemer The reasoned Schemer
Code from the books by Peteris Krumins (peter@catonmat.net). His blog is at http://www.catonmat.net/ -- good coders code, great reuse.
rslogic is a logic programming framework for Rust inspired by µKanren.
gologic includes examples
Fairness mentions early Kanren.
-
miniKanren Live and Untagged: Quine Generation via Relational Interpreters
-
μKanren: A Minimal Functional Core for Relational Programming
-
Relational Programming in miniKanren: Techniques, Applications, and Implementations
-
Pure, Declarative, and Constructive Arithmetic Relations (Declarative Pearl)
-
From Variadic Functions to Variadic Relations - A miniKanren Perspective
Plenty of other miniKanren use log-time persistent maps for their substitutions; core.logic (https://github.com/clojure/core.logic) and veneer (https://github.com/tca/veneer) certainly do.
JaCoP is a finite domain solver written in pure Java that has been in continuous development since 2001. In the yearly MiniZinc constraint challenges it has received the Silver award in the fixed category for the past three years.
Some basic testing seems to show that JaCoP is anywhere from 10X-100X faster than core.logic at solving Finite Domain problems. While there is a considerable amount of work to be done to improve the performance of core.logic's general constraint framework, it's unlikely we'll achieve JaCoP finite domain solving performance in the near future. Thus JaCoP integration is attractive.
eq is the basic goal constructor: it succeeds if its arguments unify, fails otherwise.
conde accepts two or more clauses made of lists of goals, and returns the logical disjunction of these clauses.
fresh accepts a list of one or more logic variables, and a block containing
one or more goals. The logic variables are bound into the lexical scope of the
block, and the logical conjuction of the goals is performed.
run is similar to run_all, but returns at most n results.
run_all accepts a list of one or more logic variables, an optional module name for a constraint solver, and a block containing one or more goals.
The logic variables are bound into the lexical scope of the block, and the logical conjunction of the goals is performed.
All results of the conjunction are evaluated, and are returned in terms of the first logic variable given.
ExKanren/lib/minikanren.ex
conda accepts lists of goal clauses similar to conde, but returns the result of at most one clause: the first clause to have its first goal succeed.
run_all([out, x, y]) do
conda do
[eq(1, 2), eq(out, "First clause")]
[appendo(x, y, [1, 2, 3]), eq(out, {x, "Second clause"})]
[eq(x, y), eq(x, 1), eq(out, {{x, y}, "Third clause"})]
end
end
[{[], "Second clause"}, {[1], "Second clause"}, {[1, 2], "Second clause"}, {[1, 2, 3], "Second clause"}]condu is similar to conda, but takes only a single result from the first goal of the first successful clause.
project binds the associated value (if any) of one or more logic variables into lexical scope and allows them to be operated on.
run_all([out, x, y]) do
eq(x, 3)
eq(y, 7)
project([x, y]) do
eq(x + y, out)
end
end
[10]succeed is a goal that always succeeds.
succeed is a goal that ignores its argument and always succeeds.
fail is a goal that always fails.
fail is a goal that ignores its argument and always fails.
heado relates h as the head of list ls.
tailo relates t as the tail of list ls.
conso relates h and t as the head and tail of list ls.
(Equivalent to eq([h | t], ls).)
membero relates a as being a member of the list ls.
appendo relates the list ls as the result of appending lists l1 and l2.
emptyo relates a to the empty list.
onceo accepts a goal function, and allows it to succeed at most once.
copy_term copies the term associated with x to y, replacing any fresh logic variables in x with distinct fresh variables in y.
is projects its argument b, and associates a with the result of the unary operation f.(b)
fresho succeeds if its argument is a fresh logic variable, fails otherwise.