Also filled some holiday time to implement the Ackermann function in n3 running on swipl
eye/reasoning/ackermann/ackermann.n3 at master · eyereasoner/eye (github.com)
It is so nice to see that exponentiation, tetration, pentation, etc can be implemented
in such compact way!
1 Like
Thank you for this – I’d be grateful if you could write a little bit about the significance of the Ackermann function as you see it, for us pedestrians 
1 Like
It is like what ChatGPT says:
The Ackermann function, holds paramount significance in theoretical computer science and computability theory. Formulated by Wilhelm Ackermann, it stands as a fundamental example illustrating functions that transcend primitive recursion, showcasing the existence of computable problems that defy conventional algorithmic approaches. Its rapid growth, even for small inputs, makes it a powerful tool in complexity theory, establishing lower bounds on computational complexity and emphasizing the inherent challenges in designing efficient algorithms for certain problems. The Ackermann function’s prominence extends to symbolize the limits of computability, playing a crucial role in delineating what can and cannot be algorithmically computed within the theoretical realms of computer science.
You can see the rapid growth in eye/reasoning/ackermann/ackermann-answer.n3 at master · eyereasoner/eye (github.com) where A(4,0) has a value of 2 digits, A(4,1) has a value of 5 digits and A(4,2) has a value of 19729 digits.
1 Like
Can someone explain this?
Variant 1 (1st order, with fixpoint):
ack(0,N,X) :- !, X is N+1.
ack(M,0,X) :- !, K is M-1, ack(K,1,X).
ack(M,N,X) :- J is N-1, ack(M,J,H), K is M-1, ack(K,H,X).
?- time(ack(2,2048,X)).
% 12,603,397 inferences, 0.719 CPU in 0.730 seconds
X = 4099.
?- time(ack(3,12,X)).
% 1,073,479,759 inferences, 62.969 CPU in 63.099 seconds
X = 32765.
Variant 2 (higher order, with primitive recursion):
iter(F,0,X) :- !, call(F,1,X).
iter(F,N,X) :- M is N-1, iter(F,M,Y), call(F,Y,X).
tetra(0,succ) :- !.
tetra(M,iter(F)) :- K is M-1, tetra(K, F).
?- time((tetra(2,X), call(X,2048,Y))).
% 8,402,950 inferences, 0.422 CPU in 0.424 seconds
X = iter(iter(succ)),
Y = 4099.
?- time((tetra(3,X), call(X,12,Y))).
% 715,664,093 inferences, 36.547 CPU in 36.567 seconds
X = iter(iter(iter(succ))),
Y = 32765.
Why does variant 2 take less inferences and ca. twice as fast for the examples?
Edit 31.12.2023
Side quest, just currious, can n3 express higher-order?
Notation3 Language (w3c.github.io) is first order but some built-ins like Notation3 Builtin Functions (w3c.github.io) are higher order.
That’s nice, but why n3?
Here’s the Peter-Ackermann version induced by the Meta-Interpretive Learning system Louise. The Function is in “flattened” form with compound terms (FOL functions) replaced by new literals:
==
?- list_mil_problem(ack/3).
Positive examples
-----------------
ack(s(0),s(s(0)),s(s(s(s(0))))).
Negative examples
-----------------
[]
Background knowledge
--------------------
zero/1:
zero(0).
one/1:
one(s(0)).
p/2:
p(s(0),0).
p(s(s(A)),s(A)):-p(s(A),A).
Metarules
---------
(Ack-1) ∃.P,Q,R ∀.x,y,z: P(x,y,z)← Q(x),R(z,y)
(Ack-2) ∃.P,Q ∀.x,y,z,u,v,w: P(x,y,z)← Q(x,u),Q(y,v),P(x,v,w),P(u,w,z)
(Ack-3) ∃.P,Q,R,S ∀.x,y,z,u,v: P(x,y,z)← Q(x,u),R(y),S(v),P(u,v,z)
true.
==
Learning query
--------------
==
?- time(learn(ack/3)).
ack(A,B,C):-p(A,D),p(B,E),ack(A,E,F),ack(D,F,C).
ack(A,B,C):-zero(A),p(C,B).
ack(A,B,C):-p(A,D),zero(B),one(E),ack(D,E,C).
% 42,774 inferences, 0.000 CPU in 0.009 seconds (0% CPU, Infinite Lips)
true.
==
The first link tells me:
The main characteristics of N3 are as follows:
- N3 is a superset of RDF and Turtle.
- N3 adds declarative programming.
- N3 supports quoting and describing graphs of statements.
- N3 includes builtins for accessing online knowledge.
- N3 supports a scoped version of negation-as-failure.
But I am trying to understand it step by step. Is this a kind
of combination of term logic and first order logic? For example
this part of a rule:
(2 ?Y ?Z) :ackermann ?A.
It somehow follows the pattern “subject predicate object”, but
then subject has more structure, could come from LISP. Is
N3 superset of Prolog? Can we do the following with N3,
verify this inference, instance of Modus Barbara syllogism:
All humans are mortal
Aristotele is human
----------------------------------
Aristotele is mortal
Can’t make a strong statement about N3 versus Prolog except that we compile n3 into n3p (which is a prolog intermediary) and that we can translate any Prolog into n3 (using specifiv n3 buit-ins).
Yes, triples can have lists and graph terms in any position.
The Aristotle example is like the Socrates example
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://example.org/socrates#>.
:Socrates a :Human.
:Human rdfs:subClassOf :Mortal.
{?A rdfs:subClassOf ?B. ?S a ?A} => {?S a ?B}.
You can ask the question
@prefix : <http://example.org/socrates#>.
{:Socrates a ?WHAT} => {:Socrates a ?WHAT}.
and get the answer and the proof which can be independently checked with TimBL’s Cwm saying that the proof is fine.
My bad, I copied the wrong Modus Barbara example, should read:
All humans are mortal
All greeks are humans
----------------------------------
All greeks are mortal
But there are more complicated syllogisms involving existential
quantifiers and not universal quantifiers. Is there a page somewhere
that says what logic N3 supports? And also what kind of proofs it produces?
Or are the logic and the proofs EYE specific and not specified in to N3?
Although it says, but it referes to “programming”, and not logical reasoning:
Feel free to contact the N3 W3C Community Group so that they also have the benefit of your thoughts.
Proofs are not yet in the spec but the current reason.n3 ontology was designed by the Web inventor
and also implemented by him in Cwm. It is also implemented in eye and eye-js and the proofs can be checked with the Cwm proof checker.
Excellent and it is an amazing journey with steps such as Toward proof exchange in the Semantic Web (1) (w3.org) and eye/reasoning/map at master · eyereasoner/eye (github.com)
and anything in between
Right, very similar indeed.