yarn

 

Theory

Page history last edited by Anonymous 4 yrs ago

Logic programming theory

 

Logic programs traditionally are a fragment of the first order predicate calculus. Here I'm going to deal with Datalog which is the fragment of first order predicate calculus without function symbols.

 

In a simple logic programming language such as yarn we have predicates and connectives. The operators that we need are listed as follows:

 

  • v is used for disjunction. This can be read "or".
  • & is used for conjunction. We an read this as "and".
  • ¬ is used for negation. Read this as "not".
  • :- is used for entailment

 

A query in yarn might be writen as:

 

:- (& (elephant x) (penut x))

 

This would then display a valuation on x. This valuation V is a function v:X->O where O is the set of all function symbols, and X is the set of variables, such that v(x)-> o where o satisfies the query.

 

Currently I'm using the space below as a repository for notes with the intention of structuring it better in the future.


 

Recently I realized the connection between simplicial complexes and logic programming.

 

    • NOTE: Simplices are a strict generalization of the objects described in this document. Simplicies are identical under even permutations of thier vertices, while Relations are not. However the interesting topological aspects (connection of dataflow variables) are maintained under this generalization.

 

In a simple logic programming language such as yarn we have predicates and connectives. The operators that we need are listed as follows:

 

A query in our logic programming language could be writen as follows:

 

+(X,Y,Z) is a predicate that is true if X+Y=Z. It represents addition and subtraction.

 

*(X,Y,Z) is a predicate that is true if X*Y=Z. It represents multiplication and division.

 

=(X,Y) is a predicate that is true if X=Y. It represents pointwise equality.

 

+(X,Y,Z) & *(Y,Z,W) & =(W,6)

 

The above query is a specification for a simplicial complex.

 

A similar view is available with Proof Nets

 

A drawing of the specification, and a matching simplicial complex is shown in the figure below:

 

 

More complex specifications can be devised including specifications that utilize disjunction or recursion.

 

A database can be seen as the set of simplicial complexes that arise from a set of specifications and grounded facts. This is known as a Herbrand universe. A grounded fact is a specification in which there are no variables. An example would be a Parent('Gavin','Greg') in which Gavin and Greg are related by the Parent relation.

 

A specification without varibles is a simplicial complex.

 

"do you mean is also a simplicial complex? In addition to?"

 

We can see the specifications of simplicial complexes as expressions that decide whether a given simplicial complex belongs to a language.

 

Here is an example of a recursive specfication of addition (+) using a simplicial complex for the integers.

 

s(X,Y) is a relation that is used to define the natural numbers. It is a chain of 1-simplices. s(X,X) is only true of the "zero". The chain is defined such that 1 is the entity for which s(X,Y) & s(Y,Y) is true. All the other natural numbers are defined inductively in this manner. s(X,Y) can be used to define addition in a manner similar to the method of Peano Arithmetic

 

 

The above diagram can be writen as:

 

+(X,Y,Z) ← (s(X,X) & =(Y,Z)) v (s(X,V) & +(V,W,Z) & S(W,Y))

 

Where ← is the arrow of implication. If the logic is classical then A←B corresponds to:

 

(A v ¬B)

 

Intuitively one can read this as "if we can proove B, then ¬B must be false, and therefor A is true.

 

The diagram below shows the simplicial complex that corresponds to +(3,1,4) and verifies that this is in fact true:

 

 

In the case of intuisionistic logic (which is what Yarn will implement) we can not neccessarily conclude that inability to proove a fact (inability to find a simplicial complex that meets a specification) prooves the negation of that fact. When systems take this to be the case it is called negation as failure.

 

Yarn has two ways of dealing with this. If a predicate is regular (in the sense of a Heyting Algebra) then we can view implication as identical to the classical case. The user will be able to specify that a predicate is of this variety.

 

In the general case, you must either make a seperate proof for the negation, declare the predicate regular or the system will simply infer bottom, which can be read "beats me".

 

"How does a simplex differ from an state machine diagram?"

Comments (0)

You don't have permission to comment on this page.