Skip to content

Commit

Permalink
Merge pull request #25 from brandonwillard/remove-evalt-and-earlygoal…
Browse files Browse the repository at this point in the history
…error

Remove EarlyGoalError and tuple evaluation
  • Loading branch information
brandonwillard committed Feb 24, 2020
2 parents 96bea27 + beea559 commit feb3499
Show file tree
Hide file tree
Showing 29 changed files with 801 additions and 1,582 deletions.
1 change: 1 addition & 0 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ install:
- pip install -r requirements.txt

script:
- pydocstyle kanren/
- pylint kanren/ tests/
- if [[ `command -v black` ]]; then
black --check kanren tests;
Expand Down
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ docstyle:

format:
@printf "Checking code style with black...\n"
black --check kanren/
black --check kanren/ tests/
@printf "\033[1;34mBlack passes!\033[0m\n\n"

style:
Expand Down
38 changes: 19 additions & 19 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,25 @@

Logic/relational programming in Python with [miniKanren](http://minikanren.org/).

## Installation

Using `pip`:
```bash
pip install miniKanren
```

To install from source:
```bash
git clone git@github.com:pythological/kanren.git
cd kanren
pip install -r requirements.txt
```

Tests can be run with the provided `Makefile`:
```bash
make check
```

## Motivation

Logic programming is a general programming paradigm. This implementation however came about specifically to serve as an algorithmic core for Computer Algebra Systems in Python and for the automated generation and optimization of numeric software. Domain specific languages, code generation, and compilers have recently been a hot topic in the Scientific Python community. `kanren` aims to be a low-level core for these projects.
Expand Down Expand Up @@ -112,25 +131,6 @@ We can express the grandfather relationship as a distinct relation by creating a

`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

Using `pip`:
```bash
pip install miniKanren
```

To install from source:
```bash
git clone git@github.com:pythological/kanren.git
cd kanren
pip install -r requirements.txt
```

Tests can be run with the provided `Makefile`:
```bash
make check
```

## About

This project is a fork of [`logpy`](https://github.com/logpy/logpy).
Expand Down
8 changes: 0 additions & 8 deletions doc/README.md

This file was deleted.

180 changes: 97 additions & 83 deletions doc/basic.md
Original file line number Diff line number Diff line change
@@ -1,23 +1,22 @@
kanren's Types and Common Functions
----------------------------------
# Basics of `miniKanren`

The design of kanren/miniKanren is simple. It manipulates only a few types with only a few important functions.
The design of `miniKanren` is simple. It orchestrates only a few basic operations and yields a lot!

### Terms
## Terms

Terms can be

* constants like `123` or `'cat'`
* logical variables which we denote with a tilde like `~x`
* tuples of terms like `(123, 'cat')` or `(~x, 1, (2, 3))`
- any Python object (e.g. `1`, `[1, 2]`, `object()`, etc.),
- logical variables constructed with `var`—denoted here by a tilde prefix (e.g. `~x`),
- or combinations of the two (e.g. `(1, ~x, 'cat')`)

In short, they are trees in which leaves may be either constants or variables. Constants may be of any Python type.

### Unify
## Unification

We *unify* two similar terms like `(1, 2)` and `(1, ~x)` to form a *substitution* `{~x: 2}`. We say that `(1, 2)` and `(1, ~x)` unify under the substitution `{~x: 2}`. Variables may assume the value of any term.

Unify is a function that takes two terms, `u` and `v`, and returns a substitution `s`.
`unify` is a function, provided by the [`logical-unification`](https://github.com/pythological/unification) library, that takes two terms, `u` and `v`, and returns a substitution `s`.

Examples that unify

Expand All @@ -41,110 +40,125 @@ Examples that don't unify
| (1, ~x) | (2, 2) |
| (1, 2) | (~x, ~x) |

Actually we lied, `unify` also takes a substitution as input. This allows us to keep some history around. For example
Actually we lied, `unify` also takes a substitution as input. This allows us to keep some history around. For example:

>>> unify((1, 2), (1, x), {}) # normal case
{~x: 2}
>>> unify((1, 2), (1, x), {x: 2}) # x is already two. This is consitent
{~x: 2}
>>> unify((1, 2), (1, x), {x: 3}) # x is already three. This conflicts
False
```python
>>> unify((1, 2), (1, x), {}) # normal case
{~x: 2}
>>> unify((1, 2), (1, x), {x: 2}) # x is already two. This is consitent
{~x: 2}
>>> unify((1, 2), (1, x), {x: 3}) # x is already three. This conflicts
False
```

### Reify
## Reification

Reify is the opposite of unify. `reify` transforms a term with logic variables like `(1, ~x)` and a substitution like `{~x: 2}` into a term without logic variables like `(1, 2)`.
Reification is the opposite of unification. `reify` transforms a term with logic variables like `(1, ~x)` and a substitution like `{~x: 2}` into a term without logic variables like `(1, 2)`.
```python
>>> reify((1, x), {x: 2})
(1, 2)
```

>>> reify((1, x), {x: 2})
(1, 2)

### Goals and Goal Constructors
## Goals and Goal Constructors

A *goal* is a function from one substitution to a stream of substitutions.

goal :: substitution -> [substitutions]
```
goal :: substitution -> [substitutions]
```

We make goals with a *goal constructors*. Goal constructors are the normal building block of a logical program. Lets look at the goal constructor `membero` which states that the first input must be a member of the second input (a collection).

goal = membero(x, (1, 2, 3)
```
goal = membero(x, (1, 2, 3)
```

We can feed this goal a substitution and it will give us a stream of substitutions. Here we'll feed it the substitution with no information and it will tell us that either `x` can be `1` or `x` can be `2` or `x` can be `3`

>>> for s in goal({}):
... print s
{~x: 1}
{~x: 2}
{~x: 3}

```python
>>> for s in goal({}):
... print s
{~x: 1}
{~x: 2}
{~x: 3}
```
What if we already know that `x` is `2`?

>>> for s in goal({x: 2}):
... print s
{~x: 2}
```python
>>> for s in goal({x: 2}):
... print s
{~x: 2}
```

Remember *goals* are functions from one substitution to a stream of substitutions. Users usually make goals with *goal constructors* like `eq`, or `membero`.

### Goal Combinators
### Stream Functions

After this point kanren is just a library to manage streams of substitutions.
After this point `miniKanren` is just a library to manage streams of substitutions.

For example if we know both that `membero(x, (1, 2, 3))` and `membero(x, (2, 3, 4))` then we could do something like the following:

>>> g1 = membero(x, (1, 2, 3))
>>> g2 = membero(x, (2, 3, 4))
>>> for s in g1({}):
... for ss in g2(s):
... print ss
{~x: 2}
{~x: 3}

Logic programs can have many goals in complex hierarchies. Writing explicit for loops would quickly become tedious. Instead we provide functions that conglomerate goals logically.

combinator :: [goals] -> goal

Two important logical goal combinators are logical all `lall` and logical any `lany`.

>>> g = lall(g1, g2)
>>> for s in g({}):
... print s
{~x: 2}
{~x: 3}

>>> g = lany(g1, g2)
>>> for s in g({}):
... print s
{~x: 1}
{~x: 2}
{~x: 3}
{~x: 4}

```python
>>> g1 = membero(x, (1, 2, 3))
>>> g2 = membero(x, (2, 3, 4))
>>> for s in g1({}):
... for ss in g2(s):
... print ss
{~x: 2}
{~x: 3}
```
Logic programs can have many goals in complex hierarchies. Writing explicit for loops would quickly become tedious. Instead `miniKanren` provide functions that perform logic-like operations on goal streams.

```
combinator :: [goals] -> goal
```

Two important stream functions are logical all `lall` and logical any `lany`.
```python
>>> g = lall(g1, g2)
>>> for s in g({}):
... print s
{~x: 2}
{~x: 3}

>>> g = lany(g1, g2)
>>> for s in g({}):
... print s
{~x: 1}
{~x: 2}
{~x: 3}
{~x: 4}
```

### Laziness

Goals produce a stream of substitutions. This stream is computed lazily, returning values only as they are needed. kanren depends on standard Python generators to maintain the necessary state and control flow.
Goals produce a stream of substitutions. This stream is computed lazily, returning values only as they are needed. `miniKanren` depends on standard Python generators to maintain the necessary state and control flow.

>>> stream = g({})
>>> stream
<generator object unique at 0x2e13690>
>>> next(stream)
{~x: 1}
```python
>>> stream = g({})
>>> stream
<generator object unique at 0x2e13690>
>>> next(stream)
{~x: 1}
```


### User interface
## User Interface

Traditionally programs are run with the `run` function

>>> x = var('x')
>>> run(0, x, membero(x, (1, 2, 3)), membero(x, (2, 3, 4)))
(2, 3)

```python
>>> x = var()
>>> run(0, x, membero(x, (1, 2, 3)), membero(x, (2, 3, 4)))
(2, 3)
```
`run` has an implicit `lall` for the goals at the end of the call. It `reifies` results when it returns so that the user never has to touch logic variables or substitutions.

### Conclusion
## Conclusion

These are all the fundamental concepts that exist in kanren. To summarize
These are all the fundamental concepts that exist in `miniKanren`. To summarize:

* Term: a constant, variable, or tree of terms
* Substitution: a dictionary mapping variables to terms
* Unify: A function to turn two terms into a substitution that makes them match
* Goal: A function from a substitution to a stream of substitutions
* Goal Constructor: A user-level function that defines a goal
- *Term*: a Python object, logic variable, or combination of the two
- *Substitution Map*: a dictionary mapping logic variables to terms
- *Unification*: A function that finds logic variable substitutions that make two terms equal
- *Reification*: A function that substitutes logic variables in a term with values given by a substitution map
- *Goal*: A generator function that takes a substitution and yields a stream of substitutions
- *Goal Constructor*: A user-level function that constructs and returns a goal
73 changes: 0 additions & 73 deletions doc/differences.md

This file was deleted.

0 comments on commit feb3499

Please sign in to comment.