Tail calls don't exist - So why look for them?

import java.util.Stack;

interface Term { public Term whnf(); }
class Function implements Term { public Term whnf() { return this; } public Term apply(Term value) { System.out.println("Not implemented"); return null; } }

class Apply implements Term {
  Term x, y;
  boolean computed;
  Term value;
  
  public Apply(Term x, Term y) {
    this.x = x;
    this.y = y;
    computed = false;
  }
  
  /* // This is the first version of whnf I wrote, it's buggy, it crashes with a stack overflow
  public Term whnf() {
    if(!computed) {
      x = x.whnf();
      if(x instanceof Constructor) {
        value = ((Constructor)x).add(y);
      }
      else if(x instanceof Function) {
        value = ((Function)x).apply(y);
        value = value.whnf();                // this is the recursion in question, which causes it
      }
      else {
        System.out.println("ERROR");
      }
      computed = true;
    }
    return value;
  }*/
  
  public Term whnf() {
    while(true) {           // the usual fix is to use one of javas many loop constructs instead of recursion
      if(!computed) {
        x = x.whnf();
        if(x instanceof Constructor) {
          value = ((Constructor)x).add(y);
        }
        else if(x instanceof Function) {
          value = ((Function)x).apply(y);
          if(value instanceof Apply) {
            x = ((Apply)value).x;
            y = ((Apply)value).y;
            continue;
          }
        }
        else {
          System.out.println("ERROR");
        }
        computed = true;
      }
      return value;
    }
  }
}

class Constructor implements Term {
  String name;
  Term[] args;
  
  public Constructor(String name, Term... args) {
    this.name = name;
    this.args = args;
  }
  
  public Term whnf() {
    return this;
  }
  
  public Constructor add(Term t) {
    int i; Term[] oldArgs = args;
    args = new Term[oldArgs.length+1];
    for(i = 0; i < oldArgs.length; i++)
      args[i] = oldArgs[i];
    args[i] = t;
    return this;
  }
}

class Add extends Function { public Term apply(Term value) { return new Add1(value); } }
class Add1 extends Function {
  Term x;
  public Add1(Term x) { this.x = x; }
  public Term apply(Term y) {
    x = x.whnf();
    if(((Constructor)x).name == "Z") { return y; } // add Z y = y
    else if(((Constructor)x).name == "S") {        // add (S x) y = S (add x y)
      return new Constructor("S", new Apply(new Apply(new Add(), ((Constructor)x).args[0]), y));
    }
    System.out.println("Pattern match fell through");
    return null;
  }
}

class Tail extends Function { public Term apply(Term value) { return ((Constructor)value.whnf()).args[1]; } }

class ZipWith extends Function { public Term apply(Term f) { return new ZipWith1(f); } }
class ZipWith1 extends Function { Term f; public ZipWith1(Term f) { this.f = f; } public Term apply(Term xs) { return new ZipWith2(f,xs); } }
class ZipWith2 extends Function {
  Term f, xs;
  public ZipWith2(Term f, Term xs) { this.f = f; this.xs = xs; }
  public Term apply(Term ys) {
    xs = xs.whnf();
    if(((Constructor)xs).name == "[]") return ys; // zipWith f [] y = y
    ys = ys.whnf();
    if(((Constructor)ys).name == "[]") return xs; // zipWith f x [] = x
    Term x = ((Constructor)xs).args[0]; Term y = ((Constructor)ys).args[0];
    Term xss = ((Constructor)xs).args[1]; Term yss = ((Constructor)ys).args[1];
    // zipWith f (x:xss) (y:yss) = f x y : zipWith f xss yss
    return new Constructor(":", new Apply(new Apply(f,x), y), new Apply(new Apply(new Apply(new ZipWith(), f), xss), yss));
  }
}

class F extends Function { public Term apply(Term x) { return new Apply(new F(), x); } }

interface Instruction { public void execute(Stack<Instruction> todo); }

class OpenBracket implements Instruction {
  public void execute(Stack<Instruction> todo) {
    System.out.print("(");
  }
}

class CloseBracket implements Instruction  {
  public void execute(Stack<Instruction> todo) {
    System.out.print(")");
  }
}

class EvalTerm implements Instruction {
  Term t;
  
  public EvalTerm(Term t) {
    this.t = t;
  }
  
  public void execute(Stack<Instruction> todo) {
    Constructor c = (Constructor)t.whnf();
    t = c;
    
    System.out.print(c.name + " ");
    
    todo.push(new CloseBracket());
    for(int i = c.args.length-1; i >= 0; i--) {
      todo.push(new EvalTerm(c.args[i]));
    }
    todo.push(new OpenBracket());
  }
}

class Evaluator {
  Stack<Instruction> todo;
  
  public Evaluator(Term program) {
    todo = new Stack<Instruction>();
    todo.push(new EvalTerm(program));
  }
  
  public void evaluate() {
    while(!todo.empty()) todo.pop().execute(todo);
  }
}

public class NoTCO {
  public static void main(String args[]) {
    Term one = new Apply(new Constructor("S"), new Constructor("Z"));
    Term two = new Apply(new Constructor("S"), new Apply(new Constructor("S"), new Constructor("Z")));
    Term four = new Apply(new Constructor("S"), new Apply(new Constructor("S"), new Apply(new Constructor("S"), new Apply(new Constructor("S"), new Constructor("Z")))));
    
    // 1 : 1 : zipWith (+) fibs (tail fibs)
    Term fibs =
      new Apply(new Apply(new Constructor(":"), one),
        new Apply(new Apply(new Constructor(":"), one),
          null));
    ((Apply)((Apply)fibs).y).y =
      new Apply(new Apply(new Apply(new ZipWith(), new Add()), fibs), new Apply(new Tail(), fibs));
    
    //new Evaluator(fibs).evaluate();
    new Evaluator(new Apply(new F(), new Constructor("3"))).evaluate();
    System.out.println();
  }
}


// Important thing to note is,
// 1) This code does not analyze the input program to detect and 'optimize' tail recursion
// 2) This program doesn't stack overflow when evaluating a "tail recursive" program
//
// NB. I put "tail recursive" in quotes because it's actually irrelevant that the code is what you'd call in a strict language by that term
//     as I said in my previous post, the reason it doesn't stack overflow is not at all related to that.

Tail Call Optimization doesn't exist in Haskell

It's well known that since Haskell programs are evaluated lazily, the
considerations for writing recursive code are different to those of a strict
language.

> cat (zero,plus) [] = zero
> cat (zero,plus) (x:xs) = x `plus` cat (zero,plus) xs

> cat' (zero,plus) [] acc = acc
> cat' (zero,plus) (x:xs) acc = cat' (zero,plus) xs (acc `plus` x)

> loads = [1..1000000]

*Main> cat (0,(+)) loads
*** Exception: stack overflow
*Main> cat' (0,(+)) loads 0
*** Exception: stack overflow


Since normal numbers in haskell are strict, I'm going to use lazy numbers here
(The hope is that any results should apply to lazy structures in general, and
avoid having to take strictness into account).

> data N = Z | S N     deriving Show

> zero = Z
> plus (S x) y = S (plus x y)
> plus   Z   y = y

> lots = take 1000000 . iterate S $ Z

*Main> cat (zero,plus) lots
S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S^C(S (S (S (S Interrupted.
*Main> cat' (zero,plus) lots Z
*** Exception: stack overflow


Another example is an infinite loop:

*Main> let f x = f x in f []
^CInterrupted.
*Main> let f x = f (():x) in f []
^CInterrupted.

Both continue happily, the second takes up huge amounts of memory but it does
not stack overflow.

Haskell evaluation is like graph reduction, a program is a graph which you tug
on the end until you get a weak head normal form, in these cases you never get
one, but the program/graph is stored on the heap, in the second case that data
gets bigger and bigger (it might even get swapped to the hard disk after a
while).

That's why they didn't crash, and it had nothing to do with tail calls or tail
call optimization,  cat (zero,plus) lots  didn't do any tail call and that
didn't crash. The reason any stack overflow occurs is that the program which
reduces the graph (on the heap) has a stack, that program in my case GHC is
written in C (the RTS) and when it delves deep into an expression such as
1 + (2 + (3 + (4 + ...)))   that is what builds up stack.



So why does something like:

> spam = putStr "SPAM " >> spam

never crash?

Since (>>) is in tail position (spam is not a tail call), again, tail calls have
nothing to do with this.  m >> n  in this case means do m throw away the result
then do n, it must get thrown to the garbage collector (unlike the  f (():x)
example where the value can't be collected).



That's all fine, but we still haven't been able to sum  [1..1000000]  together.
So to recap, building up a huge expression on the heap is fine (as in the
cat (zero,plus) lots  example) but walking deep into an expression without
getting any constructors is dangerous.

> kat' (zero,plus) [] acc = acc
> kat' (zero,plus) (x:xs) acc = acc'plus'x `seq` kat' (zero,plus) xs acc'plus'x
>  where acc'plus'x = acc `plus` x

*Main> cat' (0,(+)) loads 0
*** Exception: stack overflow
*Main> kat' (0,(+)) loads 0
500000500000


> -- And a huge thanks to everyone that I talked about this with
> -- for bending my mind :)

Unscrambling without Prolog

Inductive Bit : Set :=
  H  | V
| TL | TR
| BL | BR.

Definition State :=
 (Bit * Bit * Bit *
  Bit *       Bit *
  Bit * Bit * Bit)%type.

Inductive Move : State -> State -> Set :=
| refl : forall S, Move S S

| top_left : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (B, C, A,
   D,    E,
   F, G, H)

| left_down : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (F, B, C,
   A,    E,
   D, G, H)

| right_down : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (A, B, H,
   D,    C,
   F, G, E)

| bottom_left : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (A, B, C,
   D,    E,
   G, H, F)

| trans_closure : forall A M Z,
  Move A M -> Move M Z -> Move A Z.


Definition solution state := Move state (TL, H, TR,
                                         V,     V,
                                         BL, H, BR).

Theorem prolog_example :
  solution (H, BR, BL,
            H,     TL,
            TR, V, V).


unfold solution.
eapply trans_closure.
apply top_left.
change (solution (BR, BL, H, H, TL, TR, V, V)).

Ltac whack direction :=
  unfold solution;
  eapply trans_closure;
    [ apply direction
    | match goal with
        | |- Move ?x _ => change (solution x)
      end
    ].

Ltac wtop := whack top_left.
Ltac wleft := whack left_down.
Ltac wright := whack right_down.
Ltac wbottom := whack bottom_left.

wtop.
wtop.

wtop.
wtop.
wbottom.
wbottom.
wleft.
wright.
wbottom.
wbottom.
wleft.
wright.

unfold solution.

apply refl.

Qed.

Theorem automated_example :
  solution (H, BR, BL,
            H,     TL,
            TR, V, V).

Inductive Marker (A : State) : Set := mkMarker.

Ltac save_state :=
  match goal with
    | |- solution ?state =>
      let seen := fresh "seen"
        in pose (seen := mkMarker state)
  end.

Ltac check_progress :=
  match goal with
    | |- solution ?State =>
      match goal with
        | _ : Marker State |- _ =>
          pose (dead_end := True)
        | _ => idtac
      end
  end.

Ltac swtop := save_state; whack top_left; check_progress.
Ltac swleft := save_state; whack left_down; check_progress.
Ltac swright := save_state; whack right_down; check_progress.
Ltac swbottom := save_state; whack bottom_left; check_progress.

Ltac swhack n :=
  (unfold solution; apply refl) ||
    match n with
      | 0 => fail
      | S ?m => swtop; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swleft; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swright; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swbottom; pose (dead_end := False); clear dead_end; swhack m
    end.

swhack 12.

Defined.

Print automated_example.

(*
automated_example = 
let seen := mkMarker (H, BR, BL, H, TL, TR, V, V) in
trans_closure (H, BR, BL, H, TL, TR, V, V) (BR, BL, H, H, TL, TR, V, V)
  (TL, H, TR, V, V, BL, H, BR) (top_left H BR BL H TL TR V V)
  (let dead_end := False in
   let seen0 := mkMarker (BR, BL, H, H, TL, TR, V, V) in
   trans_closure (BR, BL, H, H, TL, TR, V, V) (BL, H, BR, H, TL, TR, V, V)
     (TL, H, TR, V, V, BL, H, BR) (top_left BR BL H H TL TR V V)
     (let dead_end0 := False in
      let seen1 := mkMarker (BL, H, BR, H, TL, TR, V, V) in
      trans_closure (BL, H, BR, H, TL, TR, V, V) (TR, H, BR, BL, TL, H, V, V)
        (TL, H, TR, V, V, BL, H, BR) (left_down BL H BR H TL TR V V)
        (let dead_end1 := False in
         let seen2 := mkMarker (TR, H, BR, BL, TL, H, V, V) in
         ...
*)

Require Import List.
Inductive Move2 : Set := top_left2 | left_down2 | right_down2 | bottom_left2.
Fixpoint display_moves p q (m : Move p q) : list Move2 :=
  match m with
    | refl _ => nil
    | top_left _ _ _ _ _ _ _ _ => top_left2::nil
    | left_down _ _ _ _ _ _ _ _ => left_down2::nil
    | right_down _ _ _ _ _ _ _ _ => right_down2::nil
    | bottom_left _ _ _ _ _ _ _ _ => bottom_left2::nil
    | trans_closure _ _ _ x y => display_moves _ _ x ++ display_moves _ _ y
  end.

Eval compute in (display_moves _ _ automated_example).
(*
     = top_left2
       :: top_left2
       :: left_down2
       :: top_left2
       :: right_down2
       :: top_left2
       :: top_left2
       :: bottom_left2
       :: bottom_left2
       :: left_down2
       :: right_down2
       :: right_down2
       :: nil
     : list Move2
*)

Unscrambling with Prolog

%% I'm playing this Oxyd game (inside Enigma [link])
%% One of the puzzles is this scrambled configuration

starting(([-,⌋,⌊]
         ,[-,  ⌈]
         ,[⌉,|,|])).

%% And you've to hit against the sides to unscramble it into:

solution(([⌈,-,⌉]
         ,[|,  |]
         ,[⌊,-,⌋])).

%% Then it explodes and you win a spring
%% The moves you can do are:

move(top_left,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([B,C,A]
                  ,[D,  E]
                  ,[F,G,H])).

move(left_down,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([F,B,C]
                  ,[A,  E]
                  ,[D,G,H])).

move(right_down,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([A,B,H]
                  ,[D,  C]
                  ,[F,G,E])).

move(bottom_left,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([A,B,C]
                  ,[D,  E]
                  ,[G,H,F])).

%% I want Prolog to solve this automatically for me though,
%% My first attempt is to use recursion like so,

%: solve(Win,[]) :- solution(Win).
%: solve(State,[Move|Moves]) :- move(Move,State --> Next), solve(Next,Moves).

%! ?- starting(State), solve(State,Moves).
%! ERROR: Out of local stack

%% Since Prolog searches depth first, this just kept trying top_left,
%% again and again, getting nowhere, infact it seeing the same config.
%% so I can pass along a list of seen configurations now, and fail when
%% the same one is seen twice.

%: solve(Win,[],_) :- solution(Win).
%: solve(State,[Move|Moves],Seen) :- move(Move,State --> Next), not(member(Next,Seen)), solve(Next,Moves,[State|Seen]).

%! ?- starting(State), solve(State,Moves,[State]).
%! State = ([-, '⌋', '⌊'], [-, '⌈'], ['⌉', ('|'), ('|')]),
%! Moves = [top_left, top_left, left_down, top_left, top_left, left_down, ...]

%% I got a solution this time... but it's thousands of moves, I think the puzzle can be solved
%% Within at least 10 moves, so Prolog should fail if it gets into a branch in the search tree that deep

solve(Win,[],_,_) :- solution(Win).
solve(State,[Move|Moves],Seen,Limit) :-
 move(Move,State --> Next), not(member(Next,Seen)), succ(LowerLimit,Limit), solve(Next,Moves,[State|Seen],LowerLimit).

solve(Solution) :- starting(State), solve(State,Solution,[State],10).

%! ?- solve(Moves).
%! Moves = [top_left, top_left, bottom_left, bottom_left, left_down, right_down, bottom_left,
%!          bottom_left, left_down, right_down].

Lights out solver using CLP

:- use_module(library(clpfd)).

solve(Puzzle,Solution) :-
 dimensions(Puzzle,Rows,Cols), dimensions(Solution,Rows,Cols),
 flatten(Solution,Variables), Variables ins 0..1,
 cells_of(Puzzle --> configure(Solution)), label(Variables).

configure(Solution,(X,Y,o)) :- around(X,Y,Solution,Group), off(Group).
configure(Solution,(X,Y,*)) :- around(X,Y,Solution,Group), on(Group).

on(Lights) :- sum(Lights, #=, On), 1 #= On mod 2.
off(Lights) :- sum(Lights, #=, Off), 0 #= Off mod 2.

around(X,Y,Grid,[Up,Left,Down,Right,Middle]) :-
 Yu is Y-1, Xl is X-1,
 Yd is Y+1, Xr is X+1,
 ( Grid@([Yu,X]->Up) -> true ; Up = 0 ),
 ( Grid@([Y,Xl]->Left) -> true ; Left = 0 ),
 ( Grid@([Yd,X]->Down) -> true ; Down = 0 ),
 ( Grid@([Y,Xr]->Right) -> true ; Right = 0 ),
 ( Grid@([Y,X]->Middle) -> true ; Middle = 0 ).

game([[*,o,o,o,o,o,*,o],
      [*,*,o,*,*,*,*,*],
      [*,*,o,*,*,*,o,*],
      [*,o,o,o,o,o,o,o],
      [o,*,*,o,o,o,*,*],
      [o,*,o,o,o,o,o,o],
      [*,*,*,*,*,*,o,o],
      [o,*,*,*,*,*,*,*]]).





:- op(500,xfy,@).
:- op(1050,yfx,<-).

flatten([],[]).
flatten([X|Xs],Zs) :- flatten(Xs,Ys), append(X,Ys,Zs).

flip(P,Y,X) :- call(P,X,Y).
dimensions(Grid, Rows, Cols) :- length(Grid, Rows), maplist(flip(length,Cols),Grid).

E@([]->E)         :- !.
[X|_]@([0|Ns]->E) :- !, X@(Ns->E).
[_|X]@([N|Ns]->E) :- !, N > 0, succ(M, N), X@([M|Ns]->E).

_/E@([]<-E)               :- !.
[X|Xs]/[Y|Xs]@([0|Ns]<-E) :- !, X/Y@(Ns<-E).
[X|Xs]/[X|Ys]@([N|Ns]<-E) :- !, N > 0, succ(M, N), Xs/Ys@([M|Ns]<-E).

tuple(Board,Tuples) :- tuple((0,0),Board,Tuples).
tuple(_,[],[]).
tuple((X,Y),[Row|Rows],Tuples) :-
 tuprow((X,Y),Row-Tail,Tuples),
 succ(Y,Y1), tuple((X,Y1),Rows,Tail).
tuprow(_,[]-X,X).
tuprow((I,J),[E|Es]-X,[(I,J,E)|Xs]) :- succ(I,I1),tuprow((I1,J),Es-X,Xs).

cells_of(Grid --> Pred) :- tuple(Grid, Tuples), maplist(Pred, Tuples).