koo5 / autonomic-pyco Goto Github PK

View Code? Open in Web Editor NEW

2.0 3.0 0.0 232 KB

Project AutoNomic, decentralized platform for formally verifiable applications

License: GNU Affero General Public License v3.0

HTML 0.18% CSS 0.04% JavaScript 59.93% Python 34.56% Shell 0.01% C++ 4.92% Jupyter Notebook 0.32% q 0.01% Perl 0.03%

dependent-types logic-programming semantic-web linked-data rdf n3

autonomic-pyco's Introduction

Project AutoNomic

building a decentralized platform for formally verifiable applications.

Roadmap:

At the core is a backchaining rule engine. RDF is used as input/output format, which brings about interoperability with the Semantic Web.

The reasoning capabilities and supported forms of rules correspond to Datalog+, an extension to the well-known Datalog language.

We have gone through a series of prototypes. The latest one is called pyco, and lives in this repo alongside a growing suite of testcases.

History

Similar projects

http://ceptr.org/ http://qeditas.org/ https://www.tezos.com/ https://github.com/odipar/spread/ https://github.com/unisonweb/unison

AutoNomic originally started as part of project tauchain (http://www.idni.org/), and while Ohad Asor decided to pursue a different formalism (MSOL?), AutoNomic continues with the ideas of FOL + MLTT.

pyin/pyco

the AutoNomic-pyco repo currently serves as a sort of stable branch, while development happens in "univar". for running it, python3 is best bet, it might work with 2 with some tweaks

sudo apt install python3 python3-dev virtualenv clang

on ubuntu 16.4

sudo apt-get install software-properties-common
sudo add-apt-repository ppa:ubuntu-toolchain-r/test
sudo apt-get install gcc-8 libc++abi-8-dev
wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key|sudo apt-key add -
sudo mcedit /etc/apt/sources.list
sudo apt-get install clang-8

to set up pyco, it's best to use virtualenv:

virtualenv -p python3 cpython3
. cpython3/bin/activate
pip install -r pyin/requirements_pyco.txt

then you can run it like so:

fish shell:

env PYTHONUNBUFFERED=1 ./pyin/tau2.py   "./pyco_runner.sh --novalgrind  true --nodebug true --oneword false  --profile false   " tests/clean/zzpanla/ldl0     2>&1 | tee runs/(date "+%F-%H-%M-%S") | tee runs/last

bash:

... `date "+%F-%H-%M-%S"` ...

pyco will output a trace, point your browser to the pyco_visualization directory and use , and . keys to move around the trace steps

semantics

some notes are here: https://github.com/koo5/n3-dev-testcases

we support two forms of rules,

with only universal variables
so called AE rules

On rules with existential variables: Walking the decidability line - https://www.sciencedirect.com/science/article/pii/S0004370211000397

RDFLog: It's like Datalog for RDF - https://www.cs.ox.ac.uk/publications/publication2719-abstract.html

learn more

recent irc logs are at http://loworbit.now.im/logs/AutoNomic.log.txt

introduction to FOL: https://www.coursera.org/learn/logic-introduction/

one starting point for exloring semantics of n3 can be https://github.com/w3c/N3/issues

we have many more resources for anyone curious, so come say hi in #AutoNomic on freenode.

autonomic-pyco's People

Contributors

Stargazers

Watchers

autonomic-pyco's Issues

write a mltt typechecker for the lc interpreter

--shuffle : We should ensure that we really are order-independent

Shuffle the triples in bodies and heads in some way. Ideally, we should try all permutations of the kb and query, which means all permutations of all rules, their heads, and bodies. This would take very long on more complex test cases. Might want to determine the number of possible permutations, and then complete them in random order...
Add it to tau2.py. Move the list triple-shuffling code from pyco to tau2, to happen before the shuffling, so we can get full coverage.
add a --noshuffle testcase command (like --limit, shouldbe etc) to disallow the shuffling, in tests with builtins. Alternatively, detect builtin use automatically...

better tracing for pyco

currently, pyco dumps the whole proof tree at every step, this is slow.
support for emitting incremental changes needs to be added:
add_state id with parent id
remove_state id

additionally, generating text describing bnodes is slow, it should be moved to the trace viewer. For that end,
pyco needs to output all changes to locals.

the frontend needs to use rdf.js to load up the kbdbg rules description, as emitted by pyco at startup

the frontend also needs means to go forward and backward at least between the (numbered) trace files.
at the beginning of each trace file can be a full dump.

add findall

write a lambda calculus interpreter

investigate adding support for w3c testcase syntax

tracing big test cases (ldl)

The new vue viewer works but gets easily overwhelmed by the amount of data from the ldl testcase.
It should be able to drop used elements of the steps array and re-load them from the appropriate file again if needed.
Further, we will still want to limit the amount of data displayed, and i think this would be slightly better done on the emitting side.
We have the toggle_tracing_active or something like that command. Would be good to finally change it so that it takes a bool parameter instead.
Currently, when we re-activate tracing at some further point in the reasoner run, the viewer will have no knowledge about values of vars. Same goes for if we de-activate it before a specific command and re-activate it after.
So i would add a getvalues builtin that checks out every local variable and emits its value. The viewer has to handle this.
Now i am not sure if updating the full dump functionality to work with the new viewer is strictly necessary, although it would definitely be nice.

When this is done, we should be able to automatically deactivate and activate tracing around rdf:first rdf:rest invocations coming from n3 list syntax, and well as manually around any other uninteresting parts of the proof.

Tracing in builtins still isnt implemented. They must emit their own locals address, In the cases where their locals have an unchanging layout, we could describe them for the visualizer with the rule structure. But some builtins don't have a fixed structure, and we will have to emit the exact structure when it is allocated.

FOL existentials

We need a better story on FOL existential variables. They could appear in either the body or the head of a rule. We don't support the body case. What should really happen in the head case?
Presumably, it asserts that there exists some object of given properties.
Is there a theory that allows us to specify under what conditions is this object equal to another?
http://www.lirmm.fr/~mugnier/graphik/kiabora/

...
Is there a story on supporting or not supporting complex terms? functions?

what are the objectives (mltt typechecking..)?