muk.core module

Laws

law of fresh
if x is fresh, then unify(v, x) succeeds and associates x with v
law of unify
unify(v, w) is the same as unify(w, v)
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

Commandments

second
to transform a function whose value is not a Boolean into a function whose value is a goal, add an extra argument to hold its value, replace cond with conde, and unnest each question and answer.
>>> from muk.core import *
>>> from muk.ext import *

Primitive goals and ctors

muk.core.succeed
muk.core.fail
class muk.core._disj(g1, g2, *, interleaving)[source]

A goal that is satisfiable if either goal g1 or goal g2 is satisfiable.

Formally, it produces the following states space:

\[\begin{split}\left( \begin{array}{c}s \stackrel{g_{1}}{\mapsto} \alpha \\ s \stackrel{g_{2}}{\mapsto} \beta \end{array}\right) = \left( \begin{array}{ccccc} s_{00} & s_{01} & s_{02} & s_{03} & \ldots \\ s_{10} & s_{11} & s_{12} & s_{13} & \ldots \\ \end{array}\right)\end{split}\]

enumerated using mplus according to interleaving arg.

class muk.core._conj(g1, g2, *, interleaving)[source]

A goal that is satisfiable if both goal g1 and goal g2 is satisfiable.

Formally, it produces the following states space:

\[\begin{split}s \stackrel{g_{1}}{\mapsto} \alpha = \left( \begin{array}{c}s_{0}\\s_{1}\\s_{2}\\ s_{3}\\ \ldots\end{array}\right) \stackrel{bind(\alpha, g_{2})}{\mapsto} \left( \begin{array}{ccccc} s_{00} & s_{01} & s_{02} & s_{03} & \ldots \\ s_{10} & s_{11} & s_{12} & \ldots & \\ s_{20} & s_{21} & \ldots & & \\ s_{30} & \ldots & & & \\ \ldots & & & & \\ \end{array}\right)\end{split}\]
class muk.core.fresh(f, arity=None)[source]

Introduce new logic variables according to the needs of receiver f.

If f is a thunk then fresh is equivalent to the inversion of η-rule as defined in higher-order logic:

def η_inverse(t):

    def I(s : state):
        g = t()
        yield from g(s)

    return I

having particular application in the definition of recursive relations.

class muk.core._unify(u, v, ext_s)[source]

Attempts to perform unification to make u and v unifiable given a set of associations for logic variables.

muk.core.unification(u, v, sub, ext_s)[source]

Attempts to augment substitution sub with associations that makes u unify with v.

States streams and enumerations

muk.core.mplus(streams, interleaving)[source]

It enumerates the states space streams, using different strategies according to interleaving.

In order to understand states enumeration can be helpful to use a matrix, where we associate a row to each stream of states α belonging to streams. Since streams is an iter obj over a countably, possibly infinite, set of states streams, the matrix could have infinite rows. In parallel, since each states stream α lying on a row is a iter obj over a countably, possibly infinite, set of satisfying states, the matrix could have infinite columns; therefore, the matrix we are building could be infinite in both dimensions. So, let streams be represented as follows:

\[\begin{split}\left( \begin{array}{ccccc} s_{00} & s_{01} & s_{02} & s_{03} & \ldots \\ s_{10} & s_{11} & s_{12} & \ldots & \\ s_{20} & s_{21} & \ldots & & \\ s_{30} & \ldots & & & \\ \ldots & & & & \\ \end{array}\right)\end{split}\]

In order to enumerate this infinite matrix we have the following strategies:

depth-first

Enumerates a stream α committed to it until it is saturated or continue to yield its state objects forever; in other words, it enumerates row by row. For the sake of clarity, assume the first \(k\) streams are finite and the \(k\)-th is the first to be infinite, hence we are in the following context:

\[\begin{split}\left( \begin{array}{ccccc} s_{00} & s_{01} & \ldots & s_{0i_{0}} \\ s_{10} & s_{11} & \ldots & s_{1i_{1}} \\ \ldots_{\triangle} \\ s_{k-1, 0} & s_{k-1,1} & \ldots & s_{k-1,i_{k-1}} \\ s_{k0} & s_{k1} & \ldots & \ldots & \ldots \\ s_{k+1, 0} & \ldots & & \\ \ldots & & & \\ \end{array}\right)\end{split}\]

so enumeration proceeds as follows: \(s_{00}, s_{01},\ldots, s_{0i_{0}}, s_{10}, s_{11}, \ldots, s_{1i_{1}}, \ldots_{\triangle}, s_{k-1,0}, s_{k-1, 1},\ldots, s_{k-1,i_{k-1}}, s_{k0}, s_{k1},\ldots\) yielding from stream \(\alpha_{k}\) forever, never reaching \(s_{k+1, 0}\).

breadth-first

Enumerates interleaving state objects belonging to adjacent streams, lying on the same column; in other words, it enumerates column by column. If streams is an iterator over an infinite set of streams, the it enumerates only the very first state objects, namely \(s_{00}, s_{10}, s_{20}, s_{30},\ldots\).

The following is a straighforward implementation:

from itertools import chain

while True:
    try: 
        α = next(streams)
    except StopIteration: 
        break
    else:
        try:
            s = next(α) # s : state 
        except StopIteration:
            continue
        else:
            yield s
            streams = chain(streams, [α])
dovetail

Enumerates interleaving state objects lying on the same diagonal, resulting in a fair scheduler in the sense that every satisfying state object will be reached, eventually. For the sake of clarity, enumeration proceeds as follows:

\[s_{00}, s_{10}, s_{01}, s_{20}, s_{11}, s_{02}, s_{30}, s_{21}, s_{12}, s_{03}, \ldots\]

providing a complete enumeration strategy.

Parameters:
  • stream (iter) – an iterator over a countable set of state-streams
  • interleaving (bool) – enumeration strategy selector: dovetail if interleaving else depth-first
Returns:

an iter object over satisfying state objects
muk.core.bind(α, g, *, mplus)[source]

A stream combinator, it applies goal g to each state in stream α.

Such mapping can be linear in the sense of vanilla map application:

\[\begin{split}\alpha = \left( \begin{array}{c}s_{0}\\s_{1}\\s_{2}\\ s_{3}\\ \ldots\end{array}\right) \stackrel{map(g, \alpha)}{\mapsto} \left( \begin{array}{ccccc} s_{00} & s_{01} & s_{02} & s_{03} & \ldots \\ s_{10} & s_{11} & s_{12} & \ldots & \\ s_{20} & s_{21} & \ldots & & \\ s_{30} & \ldots & & & \\ \ldots & & & & \\ \end{array}\right)\end{split}\]

After the mapping obj is built, it is consumed as argument by mplus to enumerate the states space.

Moreover, a recursive implementation can be written as found in The Reasoned Schemer, but in some cases it raises RecursionError due to Python limitation on stack usage:

try:
    s = next(α) # s : state 
except StopIteration:
    yield from fail()
else:
    β = g(s)
    γ = bind(α, g, mplus)
    yield from mplus(iter([β, γ]))

which produces the following states space:

\[\begin{split}\alpha = \left( \begin{array}{c}s_{0}\\s_{1}\\s_{2}\\ s_{3}\\ \ldots\end{array}\right) \stackrel{bind(\alpha, g)}{\mapsto} \left( \begin{array}{l} s_{00} \, s_{01} \, s_{02} \, s_{03} \, s_{04} \,s_{05} \,\ldots \\ \left( \begin{array}{l} s_{10} \, s_{11} \, s_{12} \, \ldots \, \\ \left( \begin{array}{l} s_{20} \, s_{21} \, \ldots \, \, \\ \left( \begin{array}{l} s_{30} \, \ldots \, \, \, \\ \ldots \, \, \, \, \\ \end{array}\right) \end{array}\right) \end{array}\right) \end{array}\right)\end{split}\]

assuming we want to enumerate using interleaving:

\[s_{00}, s_{10}, s_{01}, s_{20}, s_{02}, s_{11}, s_{03}, s_{30}, s_{04}, s_{12}, s_{05}, s_{21}\ldots\]

which, although complete, is unbalanced in favor of first streams.

Parameters:
  • α (iter) – an iterator over a countable set of state objects
  • g (goal) – a relation to be satisfied
  • mplus (callable) – states space enumeration strategy
Returns:

an iter object over satisfying state objects

Solver and interface

muk.core.run(goal, n=False, var_selector=<function <lambda>>, post=<function <lambda>>)[source]

Looks for a list of at most n associations [(u, v) for v in ...] such that when var u takes value v the relation goal is satisfied, where u is the main var respect the whole run invocation; otherwise, it enumerates the relation if n is False.

Parameters:goal – the relation to be satisfied respect to the main var according to var_selector.