Lambda the Ultimate

... "Something like that". Early versions of Pascal did not require the full header of a function or procedure in a parameter position. Compilers happily accepted things like

procedure p (procedure q)
  begin
    q(q)
  end;

To get the infinite loop needed for the halting problem, just write

  p(p)

It's harder to write this if you have to provide a type for p.

IIRC you can't modify the loop variable in a Pascal for-loop.

It worked on CodeIDE. That doesn't mean it would work in all Pascal variants, of course.

Edit: poking around Google shows that Pascal variants generally do not allow you to muck with index variables. So if we assume that "P" follows this restriction my loophole is closed.

I do not know Pascel. Is there any conversion of the following program to Pascel.

function P(){
Q();
}

function Q(){
P();
}

It can be generized as -
"An unsafe procedure call loop: P1->P2->...->Pn->Pi s.t. i

There is a direct Pascal translation of that - Pascal is very similar to C in a lot of ways. But the OP said no recursion. Think old school Fortran or Cobol. Modern variants of these languages do allow recursion, but older variants did not create an activation record on each entry to a function. Instead, a function had a single statically allocated spot for its variables. Any attempt to reenter a function from within its own call environment would cause an error at runtime.

There's also a large family of functions that can't expressed that way, such as Ackermann.

Yes, they can (given higher order functions).

...and that paper does not make the claim that they can. The author points out that a restricted subset of the Recursive functions are sufficient to do all of the potentially non-terminating things that we would want, while allowing proof of termination. He does NOT under any circumstances show that we can embed Recursive functions into a language only allowing Primitive Recursion.

The Ackerman example uses full Recursion that is guarded by the property that each subcase must compute a lesser parameter in some well-founded ordering. This is a standard syntactic trick used in Termination Analysis that has been used to guide the language definition.

Another (non-related) issue that I seem to remember about that paper is that he uses a potentially infinite amount of codata which did seem to be cheating a little, at the time.

As far as the original forum post goes; somebody earlier pointed out that Pascal doesn't allow overwriting loop indices. Given that the set described contained straight-line-code and static repetitions of it - the halting problem is trivially true for the set.

The paper makes the claim that Ackerman can indeed be shown to terminate. This whole thread is about functions which can be shown to terminate, and I was clarifying that a class of non-primitively recursive functions like Ackerman can also be shown to terminate.

I think that you've misread the comment that you replied to slightly. The context of the part that you quoted was "IIRC that boils down to only allowing primitive recursion, and, indeed, such programs always halt". The class of functions that you then refered to in context was not those that terminate, but those that are primitive recursive.

Specifically Ackermann was referred to as an example of something that was non-primitive recursion, not something that didn't terminate.

I think his question was slightly confusing because he's talking about the halting problem, but is really only interested in whether or not any program exists which doesn't halt. To clarify, if we let NP be the class of program that can be written in Normal Pascal, and choose a suitable equivalence relation '=', then I think he's essentially asking whether P = NP.

It's been established that P=NP. This link has a video with an explanation of the proof.

Unless you've missed part of the description that you meant the halting problem is trivial for that class of language. If every recursion is guarded by a decrease on a well-founded ordering then the class of recursions is equivalent to bounded loops - so every program trivally terminates. Or do you mean something else by "countdown parameter" ?