2つのリストを末尾再帰的にマージするには？

Question

例えば、次の関数mergeは、2つの指定された整数リストをマージするために呼び出すことができる。

fun 
merge 
{m,n:nat} 
(
xs: list(int, m) 
, 
ys: list(int, n) 
) : list(int, m+n) = 
(
    case+ xs of 
    | list_nil() => ys 
    | list_cons(x, xs2) => 
    (
     case+ ys of 
     | list_nil() => xs 
     | list_cons(y, ys2) => 
      if x <= y 
      then list_cons(x, merge(xs2, ys)) 
      else list_cons(y, merge(xs, ys2)) 
      // end of [if] 
    ) 
) 

は明らかに、mergeは末尾再帰ではありません。 2つの非常に長いリストに適用すると、mergeはコールスタックをオーバーフローする可能性があります。テール再帰的にmergeを実装する方法はありますか？ stream2list_vtはテールrecusive（と非常にメモリ-質素）であることを

Answer 1

注：

fun 
merge 
{m,n:nat} 
(
xs: list(int, m) 
, 
ys: list(int, n) 
) : List0_vt(int) = stream2list_vt(merge2(xs, ys)) 

and 
merge2 
{m,n:nat} 
(
xs0: list(int, m) 
, 
ys0: list(int, n) 
) : stream_vt(int) = $ldelay 
(
    case+ xs0 of 
    | list_nil() => 
    !(streamize_list_elt(ys0)) 
    | list_cons(x0, xs1) => 
    (
     case+ ys0 of 
     | list_nil() => 
     !(streamize_list_elt(xs0)) 
     | list_cons(y0, ys1) => 
     if x0 <= y0 
      then stream_vt_cons(x0, merge2(xs1, ys0)) 
      else stream_vt_cons(y0, merge2(xs0, ys1)) 
     // end of [if] 
    ) 
) 

上で与えられたものよりもmerge尾再帰的に実施するために、確かに、より効率的な方法があります。しかし、リニアストリームを使用するこの例は、リストを末尾再帰的に構築するための単純かつ体系的な方法を示しています。