Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!ark1!ai.etl.army.mil!hoey
From: hoey@ai.etl.army.mil (Dan Hoey)
Newsgroups: comp.lang.misc
Subject: Re: The Forbidden (previously misspelled ``Forbiden'')
Message-ID: <90@ai.etl.army.mil>
Date: 17 Aug 90 20:37:30 GMT
References: <24279@megaron.cs.arizona.edu>
Reply-To: hoey@ai.etl.army.mil (Dan Hoey)
Organization: Naval Research Laboratory, Washington, DC
Lines: 19

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