Lambda the Ultimate

Logical foundation are for axioms and Logic Programs. Logical foundations are also important for security since inconsistencies in foundations can cause security problems. At the same time foundations must be strong enough so that computers can carry out all logical reasoning including reasoning about their own reasoning processes :-)

Axioms and Logic Programs will become much more important and practical in future computer applications.

As someone learning this stuff (still...) I would like to ask a question, apologies in advance if my terminology is a bit wrong (please feel free to correct me). The contradiction in the above logic appears to come from allowing self-referential statements. It is the equivalent of the halting problem and is effectively an infinite loop in deduction. It would appear the simple solution is to stratify the logic, as done in type-theory into a stack of infinite universes, where reference to a clause in universe N automatically puts you in universe N+1. This would appear to have problems with implementing realistic programs.

The other thought is that without negation such proofs would not be possible. If proofs can only be built constructively (again like some branches of type theory) then such things would not be possible. Again this would appear to have limitations implementing realistic programs.

The approach taken by Kernel-Prolog looks interesting (with a few tweaks), which is to replace 'cut' and other builtins by meta-interpreters, which are effectively nested universes. If an interpreter does not implement failure as negation, then such contradictory proofs would not be possible inside that 'universe' and we can allow recursion. We can the close that meta-interpreter and implement negation in an outer interpreter (the next universe up).

I can already see some problems, as I have been playing with implementing Model Elimination, which mostly requires extensive use of negated predicates, but "not_p" is not the same as "\+p" which has me slightly confused at the moment.

Is there a reasonably short proof that is self contradictory that could be used as a test for this sort of thing?

According to Wittgenstein:

Let us suppose I prove the improvability (in Russell’s system) of
[Gödel's self-referential proposition] P; [⊢⊬P where P⇔⊬P]
then by this proof I have proved P [⊢P].
Now if this proof were one in Russell’s system [⊢⊢P]—I should in
this case have proved at once that it belonged [⊢P] and did not
belong [⊢¬P because ¬P⇔⊢P] to Russell’s system.
But there is a contradiction here!

The Russell paradox can be expressed in Prolog as the Barber paradox:

male(barber).
shaves(barber, X) :- male(X), \+ shaves(X,X).

It would appear Datalog already addressed this problem (in more or less the way I thought above):

If a predicate P is positively derived from a predicate Q
(i.e., P is the head of a rule, and Q occurs positively in
the body of the same rule), then the stratification
number of P must be greater than or equal to the
stratification number of Q

If a predicate P is derived from a negated predicate Q
(i.e., P is the head of a rule, and Q occurs negatively
in the body of the same rule), then the stratification
number of P must be greater than the stratification
number of Q,

So the implementation I am looking at based on kernel prolog that does not have failure-as-negation in the language, but requires you to use a meta-interpreter:

first_solution(X, G, Answer) :-
    answer_source(X, G, Solver),
    get(Solver, R),
    stop(Solver),
    eq(Answer, R).

not(G) :- first_solution(_, G, no).

The meta-interpreter runs on the same program clauses, but is initialised by answer_source(X, G, Solver) where X is the answer pattern, G is the goal, and Solver is the fluent, then get(Solver, R) gets each solution to G, until stop is called. The meta interpreter returns the(X) or no with appropriate substitutions, so not(G) is true when there are no solutions to the goal G.

So by not including the negation as failure builtin, the only way to get a 'not' relation is to use a meta-interpreter, which results in a simply implemented stratification with no special 'rules' it is just an emergent property of the language semantics.

I like this, and it seems to deal with the above problem.

The other issues can be addressed by using the techniques from PTTP (Prolog Technology Theorem Prover), which is sound unification (occurs check, I am using rational-tree unification with a post-cycle check on any repeated variables), complete inference (achieved for Model Elimination by checking the current goal against the negation of each goal in a history stack). Finally although not mentioned above, complete search by using depth-first with iterative-deepening.

Syntactic stratification is unworkable for Computer Science, e.g., it is impossible implement interpreters (i.e. Eval in Lisp).

Do you mean it is impossible to implement interpreters in Prolog? Obviously prolog itself is an interpreter, so you just make the existing interpreter available through reflection. This is quite neat as all the 'mechanics' of a Prolog implementation become available as builtins, 'copy term with fresh variables', 'unification', 'unfolding'. I guess whilst this is practical for application, it may cause problems if you are trying to use logic as the fundamental basis of computation.

An interpreter can be implemented as the transitive closure over the unfolding operation:

element_of(I, X) :- get(I, the(A)), select_from(I, A, X).
select_from(_, A, A).
select_from(I, _, X) :- element_of(I, X).

unfold(Clause, Clause).
unfold(Clause, Answer) :-
    unfolder_source(Clause, Unfolder),
    element_of(Unfolder, NewClause),
    unfold(NewClause, Answer).

So the problem must be in defining 'unfolder_source', but that is the operation:

A0 :- A1, A2,..., An (+) B0 :- B1, B2,..., Bm =mgu(A1, B0).(A0 :- B1,..., Bm, A2,..., An)

I am not sure where the difficulty in implementing that is? We can implement unification, and the remainder is simply a rearrangement.

Implementing Eval messages requires type Any as in the interface below for type Expression so that an expression receives an Eval message with an Environment and can return any value:

Expression ≡ Interface Eval[Environment]↦Any

In Prolog the type returned from the meta-interpreter is aways a term, and can be normalised to a clause. This is clearly visible in the implementation of the answer_source fluent, in fact all the source fluents only return terms (and the sinks write them). What am I missing?

A programming language without types is hopeless for practical work.

You can add types to prolog quite easily, and there is a solution to the type of the interpreter, that is to combine it with a 'case' type statement. So if you imagine a typed prolog where each functor was classified instead of f/2 it would be f/int/int. You can then pass the interpreter a functor name, and the interpreter will match the functor on return (or fail if there is no match).

a(X::int) :- ...
a(X::string) :- ...
:- first_solution(X, G, Answer), a(Answer).

So although we cannot know the type returned by the interpreter, we can know the type after matching that returned term against known clause. By passing the output term as an argument to the interpreter we avoid having any untyped terms in the language.

Edit: have fixed the syntax for the interpreter, 'X' is a variable in 'G' the goal that is returned in Answer.

Below is a simple PlusExpression:

PlusExpression[left:Expression,right:Expression]:Number ≡
   implements Expression using
      Eval[anEnvironment]→ left.Eval[anEnvironment] + right.Eval[anEnvironment]

where

Expression ≡ Interface Eval[Environment]↦Any

plusExpression(X1, G1, X2, G2, Z) :- first_answer(X1, G1, A1), first_answer(X2, G2, A2), add(A1, A2, Z).

The value returned from the interpreter would be constrained to be a type accepted by 'add' by type inference. 'X' is the variable in goal 'G' to return from the meta-interpreter. The meta-interpreter runs on the same source clause database as the 'main' interpreter (unlike 'eval'). 'add' is assumed to be a builtin, but all the arithmetic could be built up from Peano arithmetic s(s(z)) etc. Type inference seems tricky, but possible.

It occurs to me as the meta-interpreter is working on the same source clauses as the 'main' interpreter, all the type information from the type-inference pass will be available, so it should be possible to statically type type return type of the meta-interpreter and check it against the required type for add. This can be a polymorphic HM type system and could use the nice compositional algorithm with principal-typings I have discussed elsewhere. I have a Prolog(ish) interpreter I have been working on that has meta-interpreters, and I plan on adding the type-inference.

What is "first-answer" and how does it implement an "Eval" message?

Sorry, I have used first_answer, where earlier I used first_solution. To clarify I intended these to be the same. This paper explains the principle of the meta-interpreters Fluents: a Uniform Extension of Kernel Prolog for Reflection and Interoperation with External Objects