Python implementation of churiso
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
 Failed to load latest commit information. Projects domains sandbox search FactOrder.py Facts.py LICENSE README.md __init__.py catalan.py churiso.xml combinators.py lexer.py misc.py parser.py programs.py reduction.py reductionTest.py run-all.sh run.py

# pychuriso

A python implementation of ChurIso. The name "ChurIso" comes from Church Encoding, which corresponds to building a structure in a purely logical system that is Isomorphic to another system. You can read more about Church Encoding here. For an overview of combinatory logic, you should start here. ChurIso finds the mapping (with the fastest running time) of symbols to combinators that are consistent with base facts. The following is an example of which representation ChurIso finds for base facts about the Seasons:

``````(succ winter) → spring              spring := (K (K K))
(succ spring) → summer              winter := (K (S (K K) (K (K K))))
(succ summer) → fall                fall := (K K)
(succ fall) → winter                summer := K
succ := ((S ((S S) S)) K)
``````

The base facts can be encoded using S and K. The system that ChurIso finds is consistent with these base facts. In other words, reducing `succ := ((S ((S S) S)) K)` applied to `spring := (K (K K))` will yield the combinator structure of `summer := K`!

## combinators

A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments. You have already seen S and K. These are reduced as follows:

(K x y) = x
(S x y z) = (x z (y z))

Other combinators include:

(I x) = x
(B x y z) = x (y z)
(C x y z = x z y
(W x y) = x y y
(T x y) = y x
(M x) = x x

These combinators can be expressed in terms of S and K. See more about this below in the section on `combinators.py`. Other combinators cannot be expressed in terms of S and K, but can be implemented in ChurIso.

(E x y a b) `if x == y: return a else: return b`

## the facts

The base facts to be encoded are written in an input.txt file. Examples of these can be found in pychuriso/domains. Some examples of current domains are:

• boolean logic
• integers
• magnetism
• kinship
• Scheme `cons`, `cdr`, `car`
• dominance relations
• propositional logic (e.g. brown cow)
• geometry
• rock-paper-scissors
• data structures
• group theory
• same/different

There are key language features that can be used in the input file.

`unique`: each of the symbols following `unique` must be represented by distinct combinator structures.
`define`: allows you to explicitly set a combinator structure for a specified symbol.
`forall`: anything of the form specified will map to the same symbol.
`not`: negation of facts. e.g. `[not (f x) = y]`
Complex logical expressions are also allowed. (e.g. `[not (f x) in {a,b,c,d}] | (g x) = y | x = y)`
`show`: indicates to print out the solution to a new problem, given the combinators mapped to the base facts.

## parsing the input

pychuriso has a parser to handle the input.txt file. This uses regular expressions to return:

``````    defines   = {}
forall = []
uniques   = []
facts     = []
shows     = dict()
``````

Single statements are parsed using `binarize()`and are transformed into an instance of `Fact`. A `Fact` has a single application on the left-hand side (f x) and a single right-hand side outcome (e.g. = y). `Fact` has several subclasses to determine reduction code for the relationship between the lhs and rhs. These include:

NegationFact
EqualityFact
InequalityFact
InFact
DisjunctionFact
PartialEqualityFact

## reduction

As we mentioned earlier, `succ := ((S ((S S) S)) K)` applied to `spring := (K (K K))` will yield the combinator structure of `summer := K`. This reduction happens in `reduction.py`, where strings are reduced to normal form. Here, the `reduce_combinator` code specifies how each combinator is handled. By the definition of the K combinator above, `reduce_combinator` will take a string ".Kxy" and return "x". Along the way, `reduce_combinator` keeps track of how many reduction steps have been taken via `GLOBAL_REDUCE_COUNTER`. This is one measure of complexity. Note that the combinators BCTMWE have reduction routines that do not rely on S and K. This is further discussed in the section below.

## the basis

The combinator basis that you use is up to you! While traditional SKI combinatory logic is available, pychuriso also supports other combinator bases (mentioned above). For the combinators that can be expressed in terms of S and K, there is an option to use an SK basis in their reduction (and therefore in computing their complexity). There is also the option to rely on a single-step reduction routine in `reduce_combinator`. This flexibility allows you to choose how you want to measure complexity, and allows you to observe the effects of different combinator bases on generalization results. Use the command line argument `--search-basis` to denote the combinator basis you want to use (e.g. `--search-basis SKIBC`). As mentioned, BCTMW can be defined in terms of S and K (thus penalizing length/complexity in that way). They can also be primitives themselves, with only one reduction step. The convention is that combinators you wish to define in terms of SK should be followed by "sk" (case sensitive). So SKIskBskCW will include I and B in terms of SK, but C and W as primitives themselves.

## the search

Before searching, facts can be reordered to prune/optimize the search. This is done by first checking if any facts can be verified, and then by checking if any constraints can be pushed. `compute_complexity` allows us to determine how many remaining searches through combinators we need. The search will be O(`compute_complexity(defines, facts)`).

The default search is set to `block` which enumerates all solutions with an increasing depth bound that is independent on each.

## syntax highlighting

If you use kate/kwrite/kile you can copy churiso.xml to ~/.local/share/katepart5/syntax/ (Ubuntu 16.1) or /usr/share/kde4/apps/katepart/syntax/ (earlier Ubuntu)

## citation

Looking to cite pychuriso? Awesome!

``````@misc{piantadosi2016pychuriso,