Giter VIP home page Giter VIP logo

arde's Introduction

Arde - Another Rust Datalog Engine

Just a Datalog thingy for Dataloggy stuff.

TODO Docs

Head to https://arde.pages.dev to test the solver, both the async solver, and the deprecated sync solver.

Version 0.2.0

This can be thought of as an alternate version of 0.1.8 that gets the async resolver (top-down) right.

It moves the interface to use all Send + Sync types, so if you want to run !Send or !Sync storages, use 0.1.8 nonasync for now. (For this reason, the web feature was removed)

Because of this switch of focus, I won't be updating the sync solver unless very necessary. The sync solver doesn't do well with sole factless negation. It cannot solve:

c :- not d.
c?

however, the async solver can.

Both can solve

b.
c :- not d.
c?

Note about tests

As they are, they aren't perfect, because the tests are sensitive to ordering and proof branching (while programs don't actually care), so actually read what the tests are saying, because both:

expected:
A: 30, 4
actual:
A: 4, 30

and

expected:
b("s") -> a("s").
actual:
NO PROOF

are equally marked as errors.

TRACING

Be incredibly careful about enabling tracing within this crate. The traces are noisy at the trace level (for the async runner). And will take a worst-case logic bomb like damn2_async.tdt from taking around 10s on a M1 Macbook, to over a minute.

Basically, until the tracing is denoised, always use an env-filter and don't use arde at the trace level, unless you want to have the logical process dumped at you in trace form.

arde's People

Contributors

jengamon avatar

Stargazers

Natalie Cuthbert avatar

Watchers

 avatar

arde's Issues

Replace @is with @unique

@unique will be unproven if given 1 element and is only proven if every element given to it is unique from any other element given to it.

@is would be expressed as is(A, B) :- not @unique(A, B). which is not a valid rule in and of itself, and thus would actually have to be constrained by the problem.

Fix solvers

Fix the solvers to formally use modus ponens/tollens to solve the program rather than our best guess

Given:
$P \implies Q$
Tollens:
$\neg Q \therefore \neg P$
Ponens:
$P \therefore Q$

where $Q = D_1 \vee D_2 \vee D_3 \vee \dots$

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.