Skip to content

Commit

Permalink
Merge pull request #11 from brandonwillard/add-basic-graph-goals
Browse files Browse the repository at this point in the history 
Add graph goals
  • Loading branch information
@brandonwillard
brandonwillard committed Jan 1, 2020
2 parents 1058cb7 + d5972ed commit 5a96fcb
Show file tree
Hide file tree
Showing 13 changed files with 973 additions and 108 deletions.
26 changes: 23 additions & 3 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,13 +84,33 @@ We can express the grandfather relationship as a distinct relation by creating a
('Abe,')
```

## Data Structures
## Constraints

`kanren` depends on functions, tuples, dicts, and generators. There are almost no new data structures/classes in `kanren` so it is simple to integrate into preexisting code.
`kanren` provides a fully functional constraint system that allows one to restrict unification and object types:

```python
>>> from kanren.constraints import neq, isinstanceo

>>> run(0, x,
... neq(x, 1), # Not "equal" to 1
... neq(x, 3), # Not "equal" to 3
... membero(x, (1, 2, 3)))
(2,)

>>> from numbers import Integral
>>> run(0, x,
... isinstanceo(x, Integral), # `x` must be of type `Integral`
... membero(x, (1.1, 2, 3.2, 4)))
(2, 4)
```

## Graph Relations

`kanren` comes with support for relational graph operations suitable for basic symbolic algebra operations. See the examples in [`doc/graphs.md`](doc/graphs.md).

## Extending `kanren`

`kanren` uses [`multipledispatch`](http://github.com/mrocklin/multipledispatch/) and the [`logical-unification` library](https://github.com/pythological/unification) to support pattern matching on user defined types. Essentially, types that can be unified can be used with most `kanren` goals. See the [project examples](https://github.com/pythological/unification#examples) for demonstrations of how the collection of unifiable types can be extended to your use case.
`kanren` uses [`multipledispatch`](http://github.com/mrocklin/multipledispatch/) and the [`logical-unification` library](https://github.com/pythological/unification) to support pattern matching on user defined types. Essentially, types that can be unified can be used with most `kanren` goals. See the [`logical-unification` project's examples](https://github.com/pythological/unification#examples) for demonstrations of how arbitrary types can be made unifiable.

## Installation

Expand Down
195 changes: 195 additions & 0 deletions doc/graphs.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,195 @@
# Relational Graph Manipulation

In this document, we show how `kanren` can be used to perform symbolic algebra operations *relationally*.

## Setup

First, we import the necessary modules and create a helper function for pretty printing the algebraic expressions.

```python
from math import log, exp
from numbers import Real
from functools import partial
from operator import add, mul

from unification import var

from etuples.core import etuple, ExpressionTuple

from kanren import run, eq, conde, lall
from kanren.core import success
from kanren.graph import walko, reduceo
from kanren.constraints import isinstanceo

# Just some nice formatting
def etuple_str(self):
if len(self) > 0:
return f"{getattr(self[0], '__name__', self[0])}({', '.join(map(str, self[1:]))})"
else:
return 'noop'


ExpressionTuple.__str__ = etuple_str
del ExpressionTuple._repr_pretty_

```

Next, we create a simple goal constructor that implements the algebraic relations `x + x == 2 * x` and `log(exp(x)) == x` and
constrains the input types to real numbers and expression tuples from the [`etuples`](https://github.com/pythological/etuples) package.

```python
def single_math_reduceo(expanded_term, reduced_term):
"""Construct a goal for some simple math reductions."""
# Create a logic variable to represent our variable term "x"
x_lv = var()
# `conde` is a relational version of Lisp's `cond`/if-else; here, each
# "branch" pairs the right- and left-hand sides of a replacement rule with
# the corresponding inputs.
return lall(
isinstanceo(x_lv, Real),
isinstanceo(x_lv, ExpressionTuple),
conde(
# add(x, x) == mul(2, x)
[eq(expanded_term, etuple(add, x_lv, x_lv)),
eq(reduced_term, etuple(mul, 2, x_lv))],
# log(exp(x)) == x
[eq(expanded_term, etuple(log, etuple(exp, x_lv))),
eq(reduced_term, x_lv)]),
)

```

In order to obtain "fully reduced" results, we need to turn `math_reduceo` into a fixed-point-producing relation (i.e. recursive).
```python
math_reduceo = partial(reduceo, single_math_reduceo)
```

We also need a relation that walks term graphs specifically (i.e. graphs composed of operator and operand combinations) and necessarily produces its output in the form of expression tuples.
```python
term_walko = partial(walko, rator_goal=eq, null_type=ExpressionTuple)
```

## Reductions

The following example is a straight-forward reduction—i.e. left-to-right applications of the relations in `math_reduceo`—of the term `add(etuple(add, 3, 3), exp(log(exp(5))))`. This is the direction in which results are normally computed in symbolic algebra libraries.

```python
# This is the term we want to reduce
expanded_term = etuple(add, etuple(add, 3, 3), etuple(exp, etuple(log, etuple(exp, 5))))

# Create a logic variable to represent the results we want to compute
reduced_term = var()

# Asking for 0 results means all results
res = run(3, reduced_term, term_walko(math_reduceo, expanded_term, reduced_term))
```

```python
>>> print('\n'.join((f'{expanded_term} == {r}' for r in res)))
add(add(3, 3), exp(log(exp(5)))) == add(mul(2, 3), exp(5))
add(add(3, 3), exp(log(exp(5)))) == add(add(3, 3), exp(5))
add(add(3, 3), exp(log(exp(5)))) == add(mul(2, 3), exp(log(exp(5))))
```

## Expansions

In this example, we're specifying a grounded reduced term (i.e. `mul(2, 5)`) and an unground expanded term (i.e. the logic variable `q_lv`). We're essentially asking for *graphs that would reduce to `mul(2, 5)`*. Naturally, there are infinitely many graphs that reduce to `mul(2, 5)`, so we're only going to ask for ten of them; nevertheless, miniKanren is inherently capable of handling infinitely many results through its use of lazily evaluated goal streams.

```python
expanded_term = var()
reduced_term = etuple(mul, 2, 5)

# Ask for 10 results of `q_lv`
res = run(10, expanded_term, term_walko(math_reduceo, expanded_term, reduced_term))
```
```python
>>> rjust = max(map(lambda x: len(str(x)), res))
>>> print('\n'.join((f'{str(r):>{rjust}} == {reduced_term}' for r in res)))
add(5, 5) == mul(2, 5)
mul(log(exp(2)), log(exp(5))) == mul(2, 5)
log(exp(add(5, 5))) == mul(2, 5)
mul(2, log(exp(5))) == mul(2, 5)
log(exp(log(exp(add(5, 5))))) == mul(2, 5)
mul(log(exp(log(exp(2)))), log(exp(5))) == mul(2, 5)
log(exp(log(exp(log(exp(add(5, 5))))))) == mul(2, 5)
mul(2, log(exp(log(exp(5))))) == mul(2, 5)
log(exp(log(exp(log(exp(log(exp(add(5, 5))))))))) == mul(2, 5)
mul(log(exp(log(exp(log(exp(2)))))), log(exp(5))) == mul(2, 5)
```

## Expansions _and_ Reductions
Now, we set **both** term graphs to unground logic variables.

```python
expanded_term = var()
reduced_term = var()

res = run(10, [expanded_term, reduced_term],
term_walko(math_reduceo, expanded_term, reduced_term))
```

```python
>>> rjust = max(map(lambda x: len(str(x[0])), res))
>>> print('\n'.join((f'{str(e):>{rjust}} == {str(r)}' for e, r in res)))
add(~_2291, ~_2291) == mul(2, ~_2291)
~_2288() == ~_2288()
log(exp(add(~_2297, ~_2297))) == mul(2, ~_2297)
~_2288(add(~_2303, ~_2303)) == ~_2288(mul(2, ~_2303))
log(exp(log(exp(add(~_2309, ~_2309))))) == mul(2, ~_2309)
~_2288(~_2294) == ~_2288(~_2294)
log(exp(log(exp(log(exp(add(~_2315, ~_2315))))))) == mul(2, ~_2315)
~_2288(~_2300()) == ~_2288(~_2300())
log(exp(log(exp(log(exp(log(exp(add(~_2325, ~_2325))))))))) == mul(2, ~_2325)
~_2288(~_2294, add(~_2331, ~_2331)) == ~_2288(~_2294, mul(2, ~_2331))
```

The symbols prefixed by `~` are the string form of logic variables, so a result like `add(~_2291, ~_2291)` essentially means `add(x, x)` for some variable `x`. In this instance, miniKanren has used our algebraic relations in `math_reduceo` to produce more relations—even some with variable operators with multiple arities!

With additional goals, we can narrow-in on very specific types of expressions. In the following, we state that `expanded_term` must be the [`cons`](https://github.com/pythological/python-cons) of a `log` and logic variable (i.e. anything else). In other words, we're stating that the operator of `expanded_term` must be a `log`, or that we want all expressions expanding to a `log`.

```python
from kanren.goals import conso

res = run(10, [expanded_term, reduced_term],
conso(log, var(), expanded_term),
term_walko(math_reduceo, expanded_term, reduced_term))
```
```python
>>> rjust = max(map(lambda x: len(str(x[0])), res))
>>> print('\n'.join((f'{str(e):>{rjust}} == {str(r)}' for e, r in res)))
log(exp(add(~_2344, ~_2344))) == mul(2, ~_2344)
log() == log()
log(exp(~reduced_2285)) == ~reduced_2285
log(add(~_2354, ~_2354)) == log(mul(2, ~_2354))
log(exp(log(exp(add(~_2360, ~_2360))))) == mul(2, ~_2360)
log(~_2347) == log(~_2347)
log(exp(log(exp(log(exp(add(~_2366, ~_2366))))))) == mul(2, ~_2366)
log(~_2351()) == log(~_2351())
log(exp(log(exp(log(exp(log(exp(add(~_2376, ~_2376))))))))) == mul(2, ~_2376)
log(~_2347, add(~_2382, ~_2382)) == log(~_2347, mul(2, ~_2382))
```

The output contains a nullary `log` function, which isn't a valid expression. We can restrict this type of output by further stating that the `log` expression's `cdr` term is itself the result of a `cons` and, thus, not an empty sequence.

```python
exp_term_cdr = var()

res = run(10, [expanded_term, reduced_term],
conso(log, exp_term_cdr, expanded_term),
conso(var(), var(), exp_term_cdr),
term_walko(math_reduceo, expanded_term, reduced_term))
```
```python
>>> rjust = max(map(lambda x: len(str(x[0])), res))
>>> print('\n'.join((f'{str(e):>{rjust}} == {str(r)}' for e, r in res)))
log(exp(add(~_2457, ~_2457))) == mul(2, ~_2457)
log(add(~_2467, ~_2467)) == log(mul(2, ~_2467))
log(exp(~_2446)) == ~_2446
log(~_2460) == log(~_2460)
log(exp(log(exp(add(~_2477, ~_2477))))) == mul(2, ~_2477)
log(~_2464()) == log(~_2464())
log(exp(log(exp(log(exp(add(~_2487, ~_2487))))))) == mul(2, ~_2487)
log(~_2460, add(~_2493, ~_2493)) == log(~_2460, mul(2, ~_2493))
log(exp(log(exp(log(exp(log(exp(add(~_2499, ~_2499))))))))) == mul(2, ~_2499)
log(log(exp(add(~_2501, ~_2501)))) == log(mul(2, ~_2501))
```
9 changes: 5 additions & 4 deletions kanren/assoccomm.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
from unification.utils import transitive_get as walk
from unification import isvar, var

from cons.core import ConsError

from . import core
from .core import (
Expand Down Expand Up @@ -105,7 +106,7 @@ def makeops(op, lists):
>>> from kanren.assoccomm import makeops
>>> makeops('add', [(1, 2), (3, 4, 5)])
(('add', 1, 2), ('add', 3, 4, 5))
(ExpressionTuple(('add', 1, 2)), ExpressionTuple(('add', 3, 4, 5)))
"""
return tuple(l[0] if len(l) == 1 else build(op, l) for l in lists)

Expand Down Expand Up @@ -149,7 +150,7 @@ def eq_assoc(u, v, eq=core.eq, n=None):
>>> x = var()
>>> run(0, x, eq(('add', 1, 2, 3), ('add', 1, x)))
(('add', 2, 3),)
(ExpressionTuple(('add', 2, 3)),)
"""
uop, _ = op_args(u)
vop, _ = op_args(v)
Expand Down Expand Up @@ -236,7 +237,7 @@ def op_args(x):
return None, None
try:
return operator(x), arguments(x)
except NotImplementedError:
except (ConsError, NotImplementedError):
return None, None


Expand All @@ -261,7 +262,7 @@ def eq_assoccomm(u, v):
>>> e1 = ('add', 1, 2, 3)
>>> e2 = ('add', 1, x)
>>> run(0, x, eq(e1, e2))
(('add', 2, 3), ('add', 3, 2))
(ExpressionTuple(('add', 2, 3)), ExpressionTuple(('add', 3, 2)))
"""
uop, uargs = op_args(u)
vop, vargs = op_args(v)
Expand Down
6 changes: 0 additions & 6 deletions kanren/dispatch.py
View file

This file was deleted.

Loading

0 comments on commit 5a96fcb

Please sign in to comment.