🚀 go-pugleaf

In article <24279@megaron.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:

>...  It's really quite trivial to prove that recursion is
>impossible in most non-recursive programs.  The only programs where
>non-recursion cannot be proven automatically are those which have a
>recursive call in a section of code that will never be executed, but
>where the compiler cannot prove that the code will never be executed.
>Since such programs are almost guaranteed to be not what the
>programmer intended, I feel confident in saying that non-recursion can
>be automatically proven in correct non-recursive programs.

That's true of simple recursion, but mutually recursive program units
(functions or subroutines) are more problematical.  It is permissible in
(nonrecursive) Fortran to have unit A contain a call to unit B and vice versa
as long as A never calls B when A was called by B (and v.v.).  Such ``lexically
recursive'' units are useful, and their failure to perform the forbidden
dynamically recursive calls cannot be verified before run time.

Dan