login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for SandBox Tail Recursion revision 2 of 2

1 2
Editor: test1
Time: 2015/06/05 15:30:14 GMT+0
Note:

added:
Actually, when using sbcl this is an infinite loop.


changed:
-In Scheme a call summa(1000000) would cause a stack overflow, just
-as in Axiom,
In Scheme a call summa(1000000) would cause a stack overflow,
however FriCAS recognizes that 'summa' has special form
and compile it to iteration

removed:
-But summa2(1000000,0) did fail.

changed:
-is apparently treated specially by Axiom as a "recurrence
is apparently treated specially by FriCAS as a "recurrence

changed:
-Similarly a stack overflow occurs in this simpler case:
Similarly a stack overflow may occur in this simpler case:

  loop : INT -> INT
  loop (n) == loop (n)
  loop (1)

but result depends on underlying Lisp.  When using sbcl default
is to optimize tail call, but different setting or using different
Lisp can lead to stack overflow.

Let's see what happens if we tell FriCAS to interpret the function:

\begin{axiom}
)set functions compile off
\end{axiom}

\begin{axiom}
  -- a stands for accumulator
  summa3(n, a) ==
    if n=0
    then a
    else summa3(n-1, n+a)
\end{axiom}

\begin{axiom}
summa3(1000000,0)
\end{axiom}

Now this function leads to stack overflow. And similarly


changed:
-\begin{axiom}
-loop (1)
-\end{axiom}
-
-Let's see what happens if we tell Axiom to compile the function:
-
-\begin{axiom}
-)set functions compile on
-\end{axiom}
-
-\begin{axiom}
-  -- a stands for accumulator
-  summa3(n, a) ==
-    if n=0
-    then a
-    else summa3(n-1, n+a)
-\end{axiom}
-
-\begin{axiom}
-summa3(1000000,0)
-\end{axiom}
-
-Now this function returns a correct value without the stack
-overflow. And similarly
-
-\begin{axiom}
-loop : INT -> INT
-loop (n) == loop (n)
-\end{axiom}
-
-if called here with 'loop(1)' becomes an infinite loop.
-
-So it seems that perhaps the tail recursion elimination only
-works when the function is compiled unless it is recognized as
-special case of a recurrence relation.
-
-The message "Invocation history stack overflow" is actually generated
-by gcl (gcl 2.6.6 is the lisp compiler used to build Axiom on MathAction).
would give stack overflow.

So tail recursion elimination only works when the function is compiled
unless it is recognized as special case of a recurrence relation.

The message about stack overflow is actually generated by Lisp implementation.
gcl (used on MathAction in the past) printed "Invocation history stack overflow",
sbcl (currently used) prints "Control stack exhausted".

changed:
-elimination is working as expected in the case where the Axiom interpreter
elimination is working as expected in the case where the FriCAS interpreter

changed:
-That depends on the Axiom interpreter/compiler. Since Common Lisp
That depends on the FriCAS interpreter/compiler. Since Common Lisp

changed:
-However, I am not sure the above is the correct way to define
-two mutually recursive functions.
-
-**Bill Page** wrote:
-
-I think that what you are writing is correct. With Axiom from the
-most recent Patch-44 (as here on MathAction) which used gcl-2.6.6
-I tried:
-

Let's try a slightly more complicated mutual recursion:

removed:
-foo : INT -> INT
-bar : INT -> INT
-foo (n) == bar (n)
-bar (n) == foo (n)
-\end{axiom}
-
-\begin{axiom}
-foo (1)
-\end{axiom}
-
----------
-
-Expanding the compiler output above you can see that MathAction
-gets the same result as you said.
-
-But when I tried this in a separate console session in Axiom
-using exactly the same version of Axiom on the same machine as
-MathAction, Axiom returned just::
-
-   Compiling function bar with type Integer -> Integer
-
-with no other output.
-
-That behaviour is odd. It should have returned either a result
-or an error message. So I repeated the command.
-
-\begin{axiom}
-foo (1)
-\end{axiom}
-
-and got::
-
-   >> System error:
-   The function |*1;foo;1;initial| is undefined.
-
----------
-
-This time I get an error message but not the one I expected.
-I don't know what this message means. (Axiom is busted ... )
-
-Let's try a slightly more complicated mutual recursion:
-\begin{axiom}

changed:
-Axiom/GCL did not recognize this as a case where tail recursion
FriCAS/sbcl did not recognize this as a case where tail recursion

changed:
-Even this "proper" case is apparently not recognized:
But sbcl recognized "proper" case:

changed:
---------
-
-So I think your caution about tail recursion elimination not being
-guaranteed is well taken.
-
-I wonder when should expect a "Value stack overflow" instead of
-an "Invocation history stack overflow"?
-
-Thanks for your comments.
-
-Regards,
-Bill Page.
-


On Tuesday, August 30, 2005 3:44 PM Jens Axel Søgaard wrote:

I tried the following and ran out of stack space:

 loop : INT -> INT
 loop (n) == loop (n)
 loop (1)

    >> System error:
    Invocation history stack overflow.

Actually, when using sbcl this is an infinite loop.

Martin Rubey asked:

 > Although this is not a nice way for Axiom to fail, two questions:
 > 
 > * is this an instance of tail-recursion?
 > 

Yes - if tail recursion were supported, then the above would be an infinite loop. I haven't got any complaints over the wording of the error message.

 > * what result would you expect?

If tail recursion is supported, the above will result in an infinite loop.

A loose definition of a tail call is: If in the body of f, a call to g is made in a position, where the result of the call, is to be returned by f, then the call to g is a tail call.

In

fricas
summa(n) ==
    if n=0
    then 0
    else n + summa(n-1)
Type: Void

fricas
summa(10)
fricas
Compiling function summa with type Integer -> Integer
fricas
Compiling function summa as a recurrence relation.

\label{eq1}55(1)
Type: PositiveInteger?

the call to summa is not a tail cail, since the result of calling summa(n-1) needs to be added to n before a value can be returned.

On the other hand in:

fricas
-- a stands for accumulator
  summa2(n, a) ==
    if n=0
    then a
    else summa2(n-1, n+a)
Type: Void

fricas
summa2(10,0)
fricas
Compiling function summa2 with type (Integer, Integer) -> Integer

\label{eq2}55(2)
Type: PositiveInteger?

the result of calling summa2(n-1,n+a) is returned immediately as the result of summa2(n,a) and is thus a tail call.

A call is active if the function called hasn't returned yet.

Proper[1] tail recursion is supported, if an unbounded number of active tail calls only use a bounded amount of stack space.

In Scheme a call summa(1000000) would cause a stack overflow, however FriCAS recognizes that summa has special form and compile it to iteration

fricas
summa(1000000)

\label{eq3}500000500000(3)
Type: PositiveInteger?

but a call summa2(1000000,0) would work without any problems.

fricas
summa2(1000000,0)

\label{eq4}500000500000(4)
Type: PositiveInteger?

However, in some Scheme implementations one can turn the stack history on and off - so perhaps there is magic switch somewhere?

See http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs-Z-H-6.html#%_sec_3.5 for a more formal definition.

[1] Here "Proper Tail Recursion" is a technical term, and doesn't mean "tail recursion done right".


Bill Page wrote:

I think the evidence above suggests something more subtle is happening here than just tail-recursion elimination (or not). For one thing, the call to summa(1000000) did not fail with a "Invocation history stack overflow" as Jens predicted above.

The definition:

  summa(n) ==
    if n=0
    then 0
    else n + summa(n-1)

is apparently treated specially by FriCAS as a "recurrence relation" and so does not produce a stack overflow.

Similarly a stack overflow may occur in this simpler case:

loop : INT -> INT loop (n) == loop (n) loop (1)

but result depends on underlying Lisp. When using sbcl default is to optimize tail call, but different setting or using different Lisp can lead to stack overflow.

Let's see what happens if we tell FriCAS to interpret the function:

fricas
)set functions compile off

fricas
-- a stands for accumulator
  summa3(n, a) ==
    if n=0
    then a
    else summa3(n-1, n+a)
Type: Void

fricas
summa3(1000000,0)
fricas
Compiling function summa3 with type (Integer, Integer) -> Integer 
>> System error: Control stack exhausted (no more space for function call frames). This is probably due to heavily nested or infinitely recursive function calls, or a tail call that SBCL cannot or has not optimized away.
PROCEED WITH CAUTION.

Now this function leads to stack overflow. And similarly

fricas
loop : INT -> INT
Type: Void
fricas
loop (n) == loop (n)
Type: Void

would give stack overflow.

So tail recursion elimination only works when the function is compiled unless it is recognized as special case of a recurrence relation.

The message about stack overflow is actually generated by Lisp implementation. gcl (used on MathAction in the past) printed "Invocation history stack overflow", sbcl (currently used) prints "Control stack exhausted". Although the examples above seem to suggest that tail recursion elimination is working as expected in the case where the FriCAS interpreter functions are compiled, a search of the web returned the following hits which suggest that some previous versions of gcl may have had some problems with tail recursion:

So maybe there is still a problem lurking out there?

Jens Axel Søgaard wrote:

That depends on the FriCAS interpreter/compiler. Since Common Lisp doesn't guarantee proper tail recursion, it isn't an error that tail recursive code can run out of stack space in GCL. Some Common Lisp compilers make an effort to optimize som tail recursive calls, but it is usually unsafe to rely on it.

The code from SICP (which uses Scheme) that Maguire is trying is thus not supposed to work an all Common Lisp implementations.

I tried another tail recursive loop in the Octorber 2004 version:

  )set functions compile on
  foo : INT -> INT
  bar : INT -> INT
  foo (n) == bar (n)
  bar (n) == foo (n)
  foo (1)

and got a:

   >> System error:
   Value stack overflow.

Let's try a slightly more complicated mutual recursion:

fricas
)set functions compile on
foo (n) == if n>0 then bar (n-1)+1 else 0
Type: Void
fricas
bar (n) == if n>0 then foo (n-1)+1 else 0
Type: Void

fricas
foo (1)
fricas
Compiling function foo with type Integer -> NonNegativeInteger
fricas
Compiling function bar with type Integer -> NonNegativeInteger
fricas
Compiling function foo with type PositiveInteger -> 
      NonNegativeInteger

\label{eq5}1(5)
Type: PositiveInteger?
fricas
foo (100)

\label{eq6}100(6)
Type: PositiveInteger?

fricas
foo (1000000)
>> System error: Control stack exhausted (no more space for function call frames). This is probably due to heavily nested or infinitely recursive function calls, or a tail call that SBCL cannot or has not optimized away.
PROCEED WITH CAUTION.

Here is the error message which as you suggest implies that FriCAS/sbcl did not recognize this as a case where tail recursion can be eliminated.

But sbcl recognized "proper" case:

fricas
bar2 (n,a) == if n>0 then foo2 (n-1,n+a) else a
Type: Void
fricas
foo2 (n,a) == if n>0 then bar2 (n-1,n+a) else a
Type: Void

fricas
foo2(1,0)
fricas
Compiling function bar2 with type (Integer, Integer) -> Integer
fricas
Compiling function foo2 with type (Integer, Integer) -> Integer

\label{eq7}1(7)
Type: PositiveInteger?
fricas
foo2(100,0)

\label{eq8}5050(8)
Type: PositiveInteger?
fricas
foo2(10000,0)

\label{eq9}50005000(9)
Type: PositiveInteger?

fricas
foo2(1000000,0)

\label{eq10}500000500000(10)
Type: PositiveInteger?