-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
0 parents
commit ad91a8b
Showing
15 changed files
with
473 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
bin/ | ||
obj/ | ||
/packages/ | ||
riderModule.iml | ||
/_ReSharper.Caches/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,71 @@ | ||
# VeryNaiveDatalog | ||
|
||
This repository contains a naive, bottom-up implementation of Datalog's | ||
semantics in about 200 lines of C# (.NET 5) code. | ||
|
||
## Introduction | ||
|
||
A Datalog program consists of a set of *facts* and *rules*. Facts denote | ||
assertions, while rules denote relationships (from which new facts | ||
are obtainable.) | ||
|
||
The "Hello World" of Datalog is graph reachability: | ||
```datalog | ||
// Rules | ||
ancestor(x,y) :- parent(x,y). | ||
ancestor(x,y) :- ancestor(x,z), parent(z,y). | ||
// Facts | ||
parent(Homer, Lisa). | ||
parent(Homer, Bart). | ||
parent(Grampa, Homer). | ||
``` | ||
|
||
For the snippet above, running the query `?ancestor(x, Bart)` (in English: | ||
for which values of `x` does `ancestor(x,Bart)` hold?) would output 2 | ||
results, namely: | ||
|
||
* `x = Homer` | ||
* `x = Grampa` | ||
|
||
which are obtainable only by first deriving the facts | ||
`ancestor(Grampa,Homer)`, `ancestor(Homer, Bart)` and | ||
`ancestor(Grampa,Bart)`, by repeated application of the rules to the facts. | ||
|
||
|
||
## How to use | ||
|
||
The snippet above can be encoded in VeryNaiveDatalog as follows (see `EvaluatorTests.cs`): | ||
|
||
```c# | ||
// Rules | ||
var r0 = new Rule(new Atom("ancestor", new Variable("x"), new Variable("y")), | ||
new Atom("parent", new Variable("x"), new Variable("y"))); | ||
|
||
var r1 = new Rule(new Atom("ancestor", new Variable("x"), new Variable("y")), | ||
new Atom("ancestor", new Variable("x"), new Variable("z")), | ||
new Atom("parent", new Variable("z"), new Variable("y"))); | ||
|
||
var rules = new[]{r0, r1}; | ||
|
||
// Facts | ||
var f0 = new Atom("parent", new Symbol("Homer"), new Symbol("Lisa")); | ||
var f1 = new Atom("parent", new Symbol("Homer"), new Symbol("Bart")); | ||
var f2 = new Atom("parent", new Symbol("Grampa"), new Symbol("Homer")); | ||
|
||
var facts = new[]{f0, f1, f2}; | ||
|
||
// Query | ||
var q = new Atom("ancestor", new Variable("x"), new Symbol("Bart")); | ||
|
||
// Run | ||
var result = facts.Query(q, rules); | ||
``` | ||
|
||
## License | ||
|
||
Public domain (see `UNLICENSE`.) | ||
|
||
## References | ||
|
||
* [The Essence of Datalog](https://dodisturb.me/posts/2018-12-25-The-Essence-of-Datalog.html) in Mistral Contrastin's blog. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
This is free and unencumbered software released into the public domain. | ||
|
||
Anyone is free to copy, modify, publish, use, compile, sell, or | ||
distribute this software, either in source code form or as a compiled | ||
binary, for any purpose, commercial or non-commercial, and by any | ||
means. | ||
|
||
In jurisdictions that recognize copyright laws, the author or authors | ||
of this software dedicate any and all copyright interest in the | ||
software to the public domain. We make this dedication for the benefit | ||
of the public at large and to the detriment of our heirs and | ||
successors. We intend this dedication to be an overt act of | ||
relinquishment in perpetuity of all present and future rights to this | ||
software under copyright law. | ||
|
||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, | ||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF | ||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. | ||
IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR | ||
OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, | ||
ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR | ||
OTHER DEALINGS IN THE SOFTWARE. | ||
|
||
For more information, please refer to <https://unlicense.org> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
using NUnit.Framework; | ||
|
||
namespace VeryNaiveDatalog.Test | ||
{ | ||
public class EvaluatorTests | ||
{ | ||
[Test] | ||
public void Evaluator_Ancestor_Example() | ||
{ | ||
// Rules | ||
var r0 = new Rule(new Atom("ancestor", new Variable("x"), new Variable("y")), | ||
new Atom("parent", new Variable("x"), new Variable("y"))); | ||
|
||
var r1 = new Rule(new Atom("ancestor", new Variable("x"), new Variable("y")), | ||
new Atom("ancestor", new Variable("x"), new Variable("z")), | ||
new Atom("parent", new Variable("z"), new Variable("y"))); | ||
|
||
// Facts | ||
var f0 = new Atom("parent", new Symbol("Homer"), new Symbol("Lisa")); | ||
var f1 = new Atom("parent", new Symbol("Homer"), new Symbol("Bart")); | ||
var f2 = new Atom("parent", new Symbol("Grampa"), new Symbol("Homer")); | ||
|
||
// Query | ||
var q = new Atom("ancestor", new Variable("x"), new Symbol("Bart")); | ||
|
||
// Run | ||
var rules = new[] {r0, r1}; | ||
var facts = new[] {f0, f1, f2}; | ||
|
||
var result = facts.Query(q, rules); | ||
|
||
// Assert | ||
var expected0 = new Substitution() {{new Variable("x"), new Symbol("Homer")}}; | ||
var expected1 = new Substitution() {{new Variable("x"), new Symbol("Grampa")}}; | ||
var expected = new[] {expected0, expected1}; | ||
|
||
CollectionAssert.AreEquivalent(expected, result); | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
<Project Sdk="Microsoft.NET.Sdk"> | ||
|
||
<PropertyGroup> | ||
<TargetFramework>net5.0</TargetFramework> | ||
|
||
<IsPackable>false</IsPackable> | ||
</PropertyGroup> | ||
|
||
<ItemGroup> | ||
<PackageReference Include="NUnit" Version="3.12.0" /> | ||
<PackageReference Include="NUnit3TestAdapter" Version="3.16.1" /> | ||
<PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.5.0" /> | ||
</ItemGroup> | ||
|
||
<ItemGroup> | ||
<ProjectReference Include="..\VeryNaiveDatalog\VeryNaiveDatalog.csproj" /> | ||
</ItemGroup> | ||
|
||
</Project> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
|
||
Microsoft Visual Studio Solution File, Format Version 12.00 | ||
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "src", "src", "{46793EA5-A98F-4CD4-92D3-E817C8C756AB}" | ||
EndProject | ||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VeryNaiveDatalog", "VeryNaiveDatalog\VeryNaiveDatalog.csproj", "{9A88574A-514C-4352-A4D0-03F7FE515A66}" | ||
EndProject | ||
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "test", "test", "{42D62CD5-18E8-49B3-86BF-642980A5E328}" | ||
EndProject | ||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VeryNaiveDatalog.Test", "VeryNaiveDatalog.Test\VeryNaiveDatalog.Test.csproj", "{2C9B857A-237C-437E-8486-085915A7DDF3}" | ||
EndProject | ||
Global | ||
GlobalSection(SolutionConfigurationPlatforms) = preSolution | ||
Debug|Any CPU = Debug|Any CPU | ||
Release|Any CPU = Release|Any CPU | ||
EndGlobalSection | ||
GlobalSection(NestedProjects) = preSolution | ||
{9A88574A-514C-4352-A4D0-03F7FE515A66} = {46793EA5-A98F-4CD4-92D3-E817C8C756AB} | ||
{2C9B857A-237C-437E-8486-085915A7DDF3} = {42D62CD5-18E8-49B3-86BF-642980A5E328} | ||
EndGlobalSection | ||
GlobalSection(ProjectConfigurationPlatforms) = postSolution | ||
{9A88574A-514C-4352-A4D0-03F7FE515A66}.Debug|Any CPU.ActiveCfg = Debug|Any CPU | ||
{9A88574A-514C-4352-A4D0-03F7FE515A66}.Debug|Any CPU.Build.0 = Debug|Any CPU | ||
{9A88574A-514C-4352-A4D0-03F7FE515A66}.Release|Any CPU.ActiveCfg = Release|Any CPU | ||
{9A88574A-514C-4352-A4D0-03F7FE515A66}.Release|Any CPU.Build.0 = Release|Any CPU | ||
{2C9B857A-237C-437E-8486-085915A7DDF3}.Debug|Any CPU.ActiveCfg = Debug|Any CPU | ||
{2C9B857A-237C-437E-8486-085915A7DDF3}.Debug|Any CPU.Build.0 = Debug|Any CPU | ||
{2C9B857A-237C-437E-8486-085915A7DDF3}.Release|Any CPU.ActiveCfg = Release|Any CPU | ||
{2C9B857A-237C-437E-8486-085915A7DDF3}.Release|Any CPU.Build.0 = Release|Any CPU | ||
EndGlobalSection | ||
EndGlobal |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
using System; | ||
using System.Collections.Generic; | ||
using System.Linq; | ||
|
||
namespace VeryNaiveDatalog | ||
{ | ||
/// <summary> | ||
/// An atom is an expression p(t_0, t_1, ..., t_n) composed of | ||
/// a predicate name (p) and a finite list of terms (t_0, ..., t_n). | ||
/// | ||
/// Examples: | ||
/// parent(Homer, Lisa) -- parent is the predicate and Homer/Lisa are symbols. | ||
/// parent(x, Lisa) -- x is a variable. | ||
/// </summary> | ||
public class Atom | ||
{ | ||
public string Name { get; } | ||
|
||
public IList<ITerm> Terms { get; } | ||
|
||
public int Arity => Terms.Count; | ||
|
||
public Atom(string name, IEnumerable<ITerm> terms) | ||
{ | ||
Name = name; | ||
Terms = terms.ToList(); | ||
} | ||
|
||
public Atom Apply(Substitution env) => new(Name, Terms.Select(t => t.Apply(env))); | ||
|
||
public Atom(string name, params ITerm[] terms) : this(name, terms.AsEnumerable()) {} | ||
|
||
public override int GetHashCode() => HashCode.Combine(Name, Terms.Aggregate(0, HashCode.Combine)); | ||
|
||
public override bool Equals(object? obj) => | ||
obj switch | ||
{ | ||
Atom that => Name == that.Name && Terms.SequenceEqual(that.Terms), | ||
_ => false | ||
}; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,46 @@ | ||
using System.Collections.Generic; | ||
using System.Linq; | ||
|
||
namespace VeryNaiveDatalog | ||
{ | ||
/// <summary> | ||
/// A naive, bottom-up evaluator. | ||
/// </summary> | ||
public static class Evaluator | ||
{ | ||
// Applies a rule to a collection of atoms, returning the newly-derived atoms. | ||
private static IEnumerable<Atom> Apply(this Rule rule, IEnumerable<Atom> kb) | ||
{ | ||
// The initial collection of bindings from which to build upon | ||
var seed = new[] {new Substitution()}.AsEnumerable(); | ||
|
||
// Attempt to match (unify) the rule's body with the collection of atoms. | ||
// Returns all successful bindings. | ||
var matches = rule.Body.Aggregate(seed, (envs, a) => a.UnifyWith(kb, envs)); | ||
|
||
// Apply the bindings accumulated in the rule's body (the premises) to the rule's head (the conclusion), | ||
// thus obtaining the new atoms. | ||
return matches.Select(rule.Head.Apply); | ||
} | ||
|
||
// Just a lifting of Rule.Apply to an IEnumerable<Rule>. | ||
private static IEnumerable<Atom> Apply(this IEnumerable<Rule> rules, IEnumerable<Atom> kb) => rules.SelectMany(r => r.Apply(kb)); | ||
|
||
// Repeatedly applies rules to atoms until no more atoms are derivable. | ||
private static IEnumerable<Atom> Evaluate(this IEnumerable<Atom> kb, IEnumerable<Rule> rules) | ||
{ | ||
int prevSize, nextSize; | ||
do | ||
{ | ||
prevSize = kb.Count(); | ||
kb = rules.Apply(kb).Union(kb); | ||
nextSize = kb.Count(); | ||
} while (prevSize < nextSize); | ||
|
||
return kb; | ||
} | ||
|
||
public static IEnumerable<Substitution> Query(this IEnumerable<Atom> kb, Atom q, IEnumerable<Rule> rules) => | ||
q.UnifyWith(kb.Evaluate(rules), new Substitution()); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
namespace VeryNaiveDatalog | ||
{ | ||
/// <summary> | ||
/// A term is either a symbol or a variable. | ||
/// </summary> | ||
public interface ITerm | ||
{ | ||
public string Name { get; } | ||
|
||
ITerm Apply(Substitution env); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
using System; | ||
using System.Collections.Generic; | ||
using System.Linq; | ||
|
||
namespace VeryNaiveDatalog | ||
{ | ||
/// <summary> | ||
/// A rule (or [Horn] clause) is an expression A_0 :- A_1, ..., A_n | ||
/// composed of a head (A_0) and a body (A_1, ..., A_n), where A_i are atoms. | ||
/// A rule without body is called a fact. | ||
/// Examples: | ||
/// parent(Homer,Lisa) -- a fact expressing that Homer is Lisa's parent | ||
/// ancestor(x,z):-ancestor(x,y),parent(y,z) -- a rule for deducing ancestors from parents | ||
/// </summary> | ||
public class Rule | ||
{ | ||
public Atom Head { get; } | ||
public IList<Atom> Body { get; } | ||
|
||
public Rule(Atom head, IEnumerable<Atom> body) | ||
{ | ||
Head = head; | ||
Body = body.ToList(); | ||
} | ||
|
||
public Rule(Atom head, params Atom[] body) : this(head, body.AsEnumerable()) {} | ||
|
||
public override bool Equals(object? obj) => | ||
obj switch | ||
{ | ||
Rule that => Head.Equals(that.Head) && Body.SequenceEqual(that.Body), | ||
_ => false | ||
}; | ||
|
||
public override int GetHashCode() => HashCode.Combine(Head, Body); | ||
|
||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
using System; | ||
using System.Collections.Generic; | ||
using System.Linq; | ||
|
||
namespace VeryNaiveDatalog | ||
{ | ||
/// <summary> | ||
/// A substitution (or environment) denotes a mapping from variables to terms. | ||
/// </summary> | ||
public class Substitution : Dictionary<Variable, ITerm> | ||
{ | ||
public Substitution() {} | ||
public Substitution(Substitution that) : base(that) {} | ||
|
||
// The condition v != t is just to avoid inserting | ||
// redundant mappings like "x -> x". | ||
public new bool TryAdd(Variable v, ITerm t) => | ||
v != t && base.TryAdd(v, t); | ||
|
||
public override bool Equals(object? obj) => | ||
obj switch | ||
{ | ||
Substitution that => this.ToHashSet().SetEquals(that), | ||
_ => false | ||
}; | ||
|
||
public override int GetHashCode() => this.Aggregate(0, (acc, p) => HashCode.Combine(acc, p.Key, p.Value)); | ||
} | ||
} |
Oops, something went wrong.