[Haskell-cafe] Type level logic programming terminology

[oleg at pobox.com]

Most systems of (first-order) logic differentiate between function
letters (aka, symbols) and predicate letters (symbols). The former are
used to build terms; the latter build atomic formulas (which can later
be combined in more complex formulas using negation, conjunction,
disjunction, and quantification):
	http://plato.stanford.edu/entries/logic-classical/

Formulas like Even (succ zero) can be interpreted to be `true' or
`false' (alternatively: succeed or fail). In the atomic formula above,
Even is a predicate symbol. OTH, terms like `succ zero' (an
application of a function symbol succ to a constant zero) is not
interpreted as true or false: it just is.

In Prolog, there is likewise distinction between terms (which can be
compared and unified, but cannot 'fail') and goals. The following
gives a good introduction in the typed setting:

http://www.cs.mu.oz.au/research/mercury/information/doc-release/reference_manual_2.html

Incidentally, many Prolog systems also permit declarations of goals
and of terms (because it helps produce better code). Lambda-Prolog,
like Mercury, insists on declarations.

The distinction between terms and goals is a bit blurred in Prolog,
due to its reflection facilities: one can add a new term as a rule or
a fact (e.g., using assert), one can examine the rules or facts, etc.


In Haskell type-level programming:
	type              -> term
	type constructor  -> function symbol
	class name        -> predicate symbol
	class constraint  -> atomic formula (atomic goal)

There is a subset of Prolog called Datalog, which is commonly
defined as Prolog without function symbols.

Logic without function symbols is equivalent to logic with function
symbols, _provided_ we have the infinite supply of constants.
For example, Foo(f(x),g(x)) can be represented as
	exists y y'. F(x,y) & G(x,y') & Foo(y,y')
So, each function symbol f of arity n is represented as a predicate
F of arity n+1. That predicate is a functional predicate: 
for each combination of the first n arguments, there exists exactly one
object (for the last argument) that makes the predicate hold.
Since terms in logic are finite, the infinitely countable supply
of constants is enough.

In Datalog however, the extensional database is finite. 
There is a finite number of facts and hence the finite number of
constants.  That breaks the above correspondence, and so terms like
f(f(f(... x))) can no longer be emulated as the corresponding F
predicate is finite (its domain is finite). That's why in pure
Datalog (without negation or with stratified negation), termination
is assured. This is not the case in pure Prolog because of the possibility
to construct longer and longer terms like succ(succ(x)).

Regarding termination, minimal models, and the correspondence between
logic formulas (and pure, positive, stratified, etc. Datalogs) and
P-complete etc. programs, please see

http://www.csupomona.edu/~jrfisher/www/logic_topics/positive/positive.html