0

It is unknown whether the following 6-clause "pure" Prolog program halts.

:- f(s(s(s(s(s(s(s(s(N)))))))),F), m(S,S,s(F)).
    
f(o,s(o)).   
f(s(N),G) :- f(N,F), m(s(N),F,G).

m(o,_,o).    
m(s(X),Y,Z) :- a(Y,P,Z), m(X,Y,P).

a(o,Y,Y).
a(s(X),Y,s(Z)) :- a(X,Y,Z).

It is based on a conjecture, related to Brocard's Problem, that n!+1=m^2 only has solutions for n < 8.

Is there a smaller Prolog program whose halting is unknown?

Only "pure" Prolog is allowed, so library and standard predicates, numbers, not and cut are forbidden.

I examined many unsolved problems but could not find a corresponding smaller program. Brocard's Problem is also one of the smallest in: https://codegolf.stackexchange.com/questions/97004/does-the-code-terminate

EDIT: Determining if a program halts can be challenging. For example, proving that the following program does not halt requires non-trivial induction.

:-  p(f(X),f(f(Y)),f(f(b))).

p(f(a),f(X),f(f(X))).
p(f(a),f(a),f(f(X))).
p(X,f(f(Y)),X) :- p(Y,f(f(Y)),f(f(X))).
p(f(X),Y,Z) :- p(X,f(Y),f(f(Z))).
Lewis Baxter
  • 21
  • 2
  • 1
    (Sorry for these downvotes and closing, all three individuals are entirely unrelated to [tag:prolog]) – false Aug 29 '23 at 05:03
  • Is the `b` in `f(f(b))` intended? – false Sep 02 '23 at 16:20
  • Yes, if it is replaced with f(f(a)) then the program halts after a few steps. I'm glad to see you investigating this. I will be interested if you get a simple proof of non-halting. – Lewis Baxter Sep 02 '23 at 18:05
  • Your use of the term *halting*. In the context of Prolog it is rather universal and existential termination. Are you aware of the literature on it? – false Sep 02 '23 at 18:19
  • You really should make your edit a separate question where you are asking why this program does not terminate. SO has quite strict rules on such (that's why your question was also closed in the beginning). – false Sep 02 '23 at 19:13
  • ... as promise: you will get a very short proof. – false Sep 02 '23 at 19:13
  • By _halting_ I mean standard Prolog procedural semantics: sequential order of clauses and left-to-right order of clauses in the body. A link to the literature is welcome. Thanks for your suggestion about making a separate question - I will do that in future. I look forward to your very short proof. – Lewis Baxter Sep 03 '23 at 02:48

1 Answers1

0

Is there a smaller Prolog program whose halting is unknown?

It all depends on your metrics of program size. If you just take the number of clauses (or literals) but do not take the size of terms into account, then the answer is yes, there are such programs. A Turing machine can be encoded with a single (recursive) binary rule and one fact. And since you are only interested in halting, the fact is not even needed. See this question for the (idea of) the encoding.

false
  • 10,264
  • 13
  • 101
  • 209