alexprengere/FormalSystems

A Python implementation of Douglas Hofstadter formal systems, from his book "Gödel, Escher, Bach" Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information. definitions formalsystems .gitignore May 10, 2016 .travis.yml Jun 13, 2016 FormalSystemsMain.py Jun 13, 2016 LICENSE MANIFEST.in README.rst Jun 13, 2016 requirements.txt setup.py Jul 5, 2016 test_formalsystems.py

FormalSystems This is a Python implementation of Douglas Hofstadter formal systems, from his book Gödel, Escher, Bach: An Eternal Golden Braid (commonly GEB).

In fact, you may define your own formal systems using a quite simple syntax, close to free text. Examples for MIU, pg, fg and NDP formal systems from the book are implemented in directory definitions.

A main Python script gives you possibilities to play with the formal system, including:

• axiom schema support (iteration, decision procedure)
• theorem step by step generation (using different algorithms)
• theorem derivation

Formal system definition

Examples

The MIU system may be define with:

```axioms:
- MI

rules:
- x is .*, xI => xIU
- x is .*, Mx => Mxx
- x is .*, y is .*, xIIIy => xUy
- x y  .* , xUUy => xy```

The underlying syntax is YAML (see raw format). You can define one or several axioms, or even an infinite number of axioms using a schema, as in the pg formal system:

```axioms:
- x is -+, xp-gx-

rules:
- x y z are -+, xpygz => xpy-gz-```

Syntax

Axiom definitions should be formatted like this (`[]` means this is optional):

`[def_1, [def_2, ...]] expr`

Where:

• `def_i` is an optional definition of wildcard, using a regular expression, for example:
• ".*" may be anything including the empty string
• "-+" is a string composed of "-"

The definitions are written using `char [is] regexp` or `char1 char2 [are] regexp` if different wildcards have the same definition. Note that you should use only one character for wildcard definition.

• `expr` is the axiom expression

Rules for theorem production should be formatted like this:

`[def_1, [def_2, ...]] cond_1 [and cond_2 [and ...]] => th_1 [and th_2 [and ...]]`

Where:

• `def_i` is the same as before
• `cond_i` is a required theorem, in order to produce new theorems (separated by and if several conditions)
• `th_i` is a produced theorems with the rule

Installation

Install with:

`\$ python setup.py install --user`

A script should be put in `~/.local/bin`, make sure this path is in your `\$PATH`:

`\$ export PATH=\$PATH:~/.local/bin`

Tests

If installation is successful, run the tests with:

```\$ cd tests
\$ python test_formalsystems.py -v```

Main script

After installation, you should have the main script `FormalSystemsMain.py` deployed somewhere where you `\$PATH` points to, under the name `FormalSystems`. If it is not the case, you can always execute the script directly, assuming the dependencies are properly installed (just pyyaml and LEPL).

Usage of the main script is fully documented in `--help` argument.

You may generate theorems step by step if the number of axioms is finite:

```\$ FormalSystems definitions/MIU.yaml --iteration 3
> Finite number of axioms, using step algorithm

STEP 1: MI

P  (1) x is .*, xI => xIU                    for  MI                         gives  MIU
P  (2) x is .*, Mx => Mxx                    for  MI                         gives  MII
.  (3) x is .*, y is .*, xIIIy => xUy        for  MI
.  (4) x y  .* , xUUy => xy                  for  MI

STEP 2: MIU/MII

P  (1) x is .*, xI => xIU                    for  MII                        gives  MIIU
.  (1) x is .*, xI => xIU                    for  MIU
P  (2) x is .*, Mx => Mxx                    for  MII                        gives  MIIII
P  (2) x is .*, Mx => Mxx                    for  MIU                        gives  MIUIU
.  (3) x is .*, y is .*, xIIIy => xUy        for  MII
.  (3) x is .*, y is .*, xIIIy => xUy        for  MIU
.  (4) x y  .* , xUUy => xy                  for  MII
.  (4) x y  .* , xUUy => xy                  for  MIU

STEP 3: MIIU/MIIII/MIUIU```

Or using a bucket where axioms are thrown and theorems computed iteratively if the number of axioms is infinite:

```\$ FormalSystems definitions/pg.yaml --iteration 4
> Infinite number of axioms, using bucket algorithm

=== BUCKET 1: -p-g--

P  (1) x y z are -+, xpygz => xpy-gz-        for  -p-g--                     gives  -p--g---

=== BUCKET 2: -p--g---/--p-g---

P  (1) x y z are -+, xpygz => xpy-gz-        for  -p--g---                   gives  -p---g----
P  (1) x y z are -+, xpygz => xpy-gz-        for  --p-g---                   gives  --p--g----

=== BUCKET 3: -p---g----/--p--g----/---p-g----

P  (1) x y z are -+, xpygz => xpy-gz-        for  -p---g----                 gives  -p----g-----
P  (1) x y z are -+, xpygz => xpy-gz-        for  ---p-g----                 gives  ---p--g-----
P  (1) x y z are -+, xpygz => xpy-gz-        for  --p--g----                 gives  --p---g-----

=== BUCKET 4: -p----g-----/---p--g-----/--p---g-----/----p-g-----```

Options are available to display theorem derivation as well:

```\$ FormalSystems definitions/NDP.yaml --quiet --derivation P-----
> Infinite number of axioms, using bucket algorithm
> Rule with several parents, using recursivity

=== BUCKET 1: --NDP-
=== BUCKET 2: --NDP---/-SD--/P--
=== BUCKET 3: --NDP-----/---SD--/---NDP--
=== BUCKET 4: --NDP-------/---NDP-----/-----SD--/P---/---NDP-
=== BUCKET 5: --NDP---------/---NDP--------/---NDP----/-------SD--/-----SD---/-SD---/----NDP---
=== BUCKET 6: ---NDP-----------/----NDP-------/---NDP-------/--NDP-----------/---------SD--/----NDP-
=== BUCKET 7: ----NDP-----------/----NDP-----/---NDP----------/---NDP--------------/--NDP-------------/-----------SD--/-------SD---/-SD----/----NDP--
=== BUCKET 8: ----NDP---------/----NDP---------------/---NDP-------------/---NDP-----------------/--NDP---------------/----NDP------/-------------SD--/-------SD----/-----SD----/-----------SD---/-----NDP-
=== BUCKET 9: --NDP-----------------/-----NDP------/----NDP-------------/---NDP--------------------/---NDP----------------/----NDP----------/----NDP-------------------/---------------SD--/-SD-----/-------------SD---/-----------SD----/P-----/-----NDP--

=== Theorem P----- found, derivation:
[1 ]  Axiom                                                                     gives  --NDP-
[2 ]  (1) x y are -+, xNDPy => xNDPxy           for  --NDP-                     gives  --NDP---
[3 ]  Axiom                                                                     gives  ---NDP--
[3 ]  (1) x y are -+, xNDPy => xNDPxy           for  --NDP---                   gives  --NDP-----
[4 ]  Axiom                                                                     gives  ----NDP-
[4 ]  (1) x y are -+, xNDPy => xNDPxy           for  ---NDP--                   gives  ---NDP-----
[4 ]  (2) z is -+, --NDPz => zSD--              for  --NDP-----                 gives  -----SD--
[5 ]  (1) x y are -+, xNDPy => xNDPxy           for  ----NDP-                   gives  ----NDP-----
[5 ]  (3) x z are -+, zSDx and x-NDPz => zSDx-  for  -----SD-- and ---NDP-----  gives  -----SD---
[6 ]  (3) x z are -+, zSDx and x-NDPz => zSDx-  for  -----SD--- and ----NDP-----  gives  -----SD----
[7 ]  (4) z is -+, z-SDz => Pz-                 for  -----SD----                gives  P-----```

Python API

Some tests using doctests:

`>>> from formalsystems.formalsystems import FormalSystem, Theorem`

MIU formal system:

```>>> fs = FormalSystem()
>>> r = fs.apply_rules_step(fs.iterate_over_schema(), step=4, verbose=False)
STEP 1: MI
STEP 2: MIU/MII
STEP 3: MIIU/MIIII/MIUIU
STEP 4: MIIIIU/MIIIIIIII/MIIUIIU/MIUIUIUIU/MIU/MUI
>>> print [str(a) for a in fs.iterate_over_schema()]
['MI']```

pg formal system:

```>>> fs = FormalSystem()
>>> r = fs.apply_rules_bucket_till(fs.iterate_over_schema(), max_turns=4, verbose=False)
=== BUCKET 1: -p-g--
=== BUCKET 2: -p--g---/--p-g---
=== BUCKET 3: -p---g----/--p--g----/---p-g----
=== BUCKET 4: -p----g-----/---p--g-----/--p---g-----/----p-g-----
>>> r = fs.apply_rules_bucket_till(fs.iterate_over_schema(), min_len=9, verbose=False)
=== BUCKET 1: -p-g--
=== BUCKET 2: -p--g---/--p-g---
=== BUCKET 3: -p---g----/--p--g----/---p-g----```

NDP formal system:

```>>> fs = FormalSystem()
>>> r = fs.apply_rules_bucket_till(fs.iterate_over_schema(), max_turns=2, full=True, verbose=False)
=== BUCKET 1: --NDP-
=== BUCKET 2: --NDP---/-SD--/P--```

Successful derivation:

```>>> fs = FormalSystem()
>>> r = fs.derivation_asc(fs.iterate_over_schema(), Theorem('P-----'), full=True, max_turns=10)
<BLANKLINE>
...
=== Theorem P----- found, derivation:
...```

Failed derivation:

```>>> fs = FormalSystem()