CIS 700 Notes: 8/27/20

basic.dl

.decl Edge(x:number,y:number)
.output Edge

// Facts
Edge(0,1).
Edge(1,2).
Edge(1,3).
Edge(3,0).

// Rule
.decl Path(x:number,y:number)
.output Path

// Whenever there's a path between z and y, and there's an edge
// between x and z, then there's a path between x and y
Path(x,y) :- Edge(x,y).
Path(x,y) :- Edge(x,z), Path(z,y).

// We might try...
//Path(x,y) :- !Edge(x,y).

.decl EdgeArgument(x:number)
EdgeArgument(x) :- Edge(x,_).
EdgeArgument(x) :- Edge(_,x).

// Invalid, because x and y are not ground
.decl NotPath(x:number, y:number)
.output NotPath
NotPath(x,y) :- EdgeArgument(y), EdgeArgument(x), !Path(x,y).

// But we get...
//Error: Ungrounded variable x in file basic.dl at line 16
//Path(x,y) :- !Edge(x,y).
//-----^-------------------
//Error: Ungrounded variable y in file basic.dl at line 16
//Path(x,y) :- !Edge(x,y).
//-------^-----------------
//2 errors generated, evaluation aborted

.type String

// (Stratified) Negation..
.decl Day(d:String)
Day("monday").
Day("tuesday").
Day("wednesday").
Day("thursday").

.decl Rainy(d:String)
Rainy("tuesday").
Rainy("thursday").

.decl GoodDay(d:String)
.output GoodDay
GoodDay(d) :- !Rainy(d), Day(d).

// All Datalog rules are "Horn Clauses" of the form...

// Head  <- Body 0   , and Body 1, and ...
//   v
H(x,...) :- B0(x,...), B1(x,...), ..., BN(x,...)

// H(x,...) \/ ~B0(x, ...) \/ ~B1(x, ...) \/ ... \/ ~BN(x, ...)

// CNF: Conjuctive Normal-Form
// Conjunction of Disjunctions
//
// This is in CNF because it's a conjunction of disjunctions:
//      (P \/ ~A)
//  /\  (~P \/ B)
//  /\  (C \/ ~B)
//  This statement is valid when..
//
// An "interpretation" is a set of predicates that are assigned
// "true." (Assume everything else is false, this is the closed-world
// assumption, CWA)
// Example valid interpretations:
// {P, B, C}
// {B, C}

// A "horn clause" is a formula written using only disjunctions and
// negation, which includes at most one positive atom.
//
// H \/ ~B0 \/ ~B1 \/ ... \/ ~Bn
// H \/ ~ (B0 /\ B1 /\ ... /\ Bn)
// ...
//
// This is equivalent to...
// B0 /\ B1 /\ ... /\ Bn -> H
// By convention in Datalog we write...
// H <- B0 /\ B1 /\ ... /\ Bn
//
// If I want to solve these types of constraints, I can perform "unit
// propagation."
//
// A "horn-SAT program" is a program written using only Horn clauses...
// H0 <- B00 /\ B01 /\ ... /\ B0n
// H1 <- B10 /\ B11 /\ ... /\ B1n
// ...
//
// There's a really elegant proof procedure for this class of
// programs, and it corresponds precisely to Datalog.
//
// How do I do it?
//
// - Start with the atomic facts, (i.e., the EDB).
// - Every atomic fact is "true"
//
// - In a loop... (until I reach a fixed-point...)
//
//   - Apply unit propagation to each rule. If the rule forces the addition of
//   new facts, add them to the database
//   (As Davis points out, this is the `cons` operator in the paper)
//
//   - When no new facts are discovered upon an iteration of this loop, you're done!
//
//   - When new facts discovered, keep going...
//
// Next week we'll talk about Souffle, an efficient implementation of this loop...