[lang0] test about equivalent between recursive functions

Author: xieyuheng

TODO.md

@@ -2,7 +2,8 @@
 
 > 支持直接递归函数与相互递归函数，不能判断等价的地方就不判断。
 
-[lang0] test about equivalent between recursive functions
+[lang0] 学习 prolog 处理递归 term unification without occor check 的方式，
+实现更好的 definitional equivalence。
 
 [lang0] 用中文重新整理 lambda encoding 相关的知识，形成一本书。
 [lang0] 用中文重新整理 lambda encoding 和 self type 相关的知识。

docs/lang0/examples/factorial.scm

@@ -11,6 +11,17 @@
 
 factorial
 
+(assert-equal factorial factorial)
+
+(assert-equal
+  factorial
+  (lambda (x) (factorial x))
+  (lambda (y) (factorial y)))
+
+(assert-equal
+  (lambda (x) (factorial x))
+  factorial)
+
 (assert-equal (factorial zero) one)
 (assert-equal (factorial one) one)
 (assert-equal (factorial two) two)

docs/lang0/examples/nat-even-odd.scm

@@ -11,6 +11,9 @@
   (if (zero? n) false
       (even? (sub1 n))))
 
+(assert-equal even? even?)
+(assert-equal odd? odd?)
+
 (assert-equal
   (even? zero)
   (even? two)

src/lang0/actions/doAp.ts

@@ -15,6 +15,8 @@ export function doAp(target: Value, arg: Value): Value {
     }
 
     case "FnRecursive": {
+      arg = Values.lazyActiveDeep(arg)
+
       if (arg["@kind"] === "NotYet") {
         return Values.NotYet(Neutrals.ApRecursive(target, arg.neutral))
       }

src/lang0/equivalent/equivalent.ts

@@ -10,8 +10,12 @@ export function equivalent(
   left: Value,
   right: Value,
 ): boolean {
-  left = prepare(left)
-  right = prepare(right)
+  left = Values.lazyActiveDeep(left)
+  right = Values.lazyActiveDeep(right)
+
+  if (right["@kind"] === "FnRecursive" && left["@kind"] === "FnRecursive") {
+    return left.name === right.name && left.mod === right.mod
+  }
 
   switch (left["@kind"]) {
     case "NotYet": {
@@ -21,32 +25,17 @@ export function equivalent(
       )
     }
 
-    case "Fn": {
+    case "Fn":
+    case "FnRecursive": {
       const freshName = freshen(ctx.usedNames, left.name)
       ctx = ctx.useName(freshName)
       const v = Neutrals.Var(freshName)
       const arg = Values.NotYet(v)
       return equivalent(ctx, Actions.doAp(left, arg), Actions.doAp(right, arg))
     }
 
-    case "FnRecursive": {
-      return (
-        right["@kind"] === "FnRecursive" &&
-        left.name === right.name &&
-        left.mod === right.mod
-      )
-    }
-
     case "Lazy": {
       return equivalent(ctx, Values.lazyActive(left), right)
     }
   }
 }
-
-function prepare(value: Value): Value {
-  if (value["@kind"] === "Lazy") {
-    return prepare(Values.lazyActive(value))
-  }
-
-  return value
-}

src/lang0/value/lazyActive.ts

@@ -11,3 +11,11 @@ export function lazyActive(lazy: Values.Lazy): Value {
   lazy.cache = value
   return value
 }
+
+export function lazyActiveDeep(value: Value): Value {
+  if (value["@kind"] === "Lazy") {
+    return lazyActiveDeep(lazyActive(value))
+  }
+
+  return value
+}