ackermann.trig

# ------------------
# Ackermann function
# ------------------
#
# 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.
#
# One can see the rapid growth in
# https://github.com/eyereasoner/eye/blob/master/reasoning/ackermann/ackermann-answer.n3
# 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.

@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix var: <http://www.w3.org/2000/10/swap/var#>.
@prefix : <http://example.org/#>.

# ackermann(x, y)
_:bng_1 log:isImpliedBy _:bng_2.

_:bng_1 {
    (var:X var:Y) :ackermann var:A.
}

_:bng_2 {
    (var:Y 3) math:sum var:B.
    (var:X var:B 2) :ackermann var:C.
    (var:C 3) math:difference var:A.
}

# ackermann(x, y, z)
# succ (x=0)
_:bng_3 log:isImpliedBy _:bng_4.

_:bng_3 {
    (0 var:Y var:Z) :ackermann var:A.
}

_:bng_4 {
    [] rdf:value true; log:callWithCut true.
    (var:Y 1) math:sum var:A.
}

# sum (x=1)
_:bng_5 log:isImpliedBy _:bng_6.

_:bng_5 {
    (1 var:Y var:Z) :ackermann var:A.
}

_:bng_6 {
    [] rdf:value true; log:callWithCut true.
    (var:Y var:Z) math:sum var:A.
}

# product (x=2)
_:bng_7 log:isImpliedBy _:bng_8.

_:bng_7 {
    (2 var:Y var:Z) :ackermann var:A.
}

_:bng_8 {
    [] rdf:value true; log:callWithCut true.
    (var:Y var:Z) math:product var:A.
}

# exponentiation (x=3), tetration (x=4), pentation (x=5), hexation (x=6), etc
_:bng_9 log:isImpliedBy _:bng_10.

_:bng_9 {
    (var:X 0 var:Z) :ackermann 1.
}

_:bng_10 {
    [] rdf:value true; log:callWithCut true.
}

_:bng_11 log:isImpliedBy _:bng_12.

_:bng_11 {
    (var:X var:Y var:Z) :ackermann var:A.
}

_:bng_12 {
    (var:Y 1) math:difference var:B.
    (var:X var:B var:Z) :ackermann var:C.
    (var:X 1) math:difference var:D.
    (var:D var:C var:Z) :ackermann var:A.
}

# query
_:bng_14 log:query _:bng_14.

_:bng_14 {
    (0 0) :ackermann var:A0.
    (0 6) :ackermann var:A1.
    (1 2) :ackermann var:A2.
    (1 7) :ackermann var:A3.
    (2 2) :ackermann var:A4.
    (2 9) :ackermann var:A5.
    (3 4) :ackermann var:A6.
    (3 14) :ackermann var:A7.
    (4 0) :ackermann var:A8.
    (4 1) :ackermann var:A9.
    #(4 2) :ackermann var:A10.
}