ambr equivalent equal

Author: xieyuheng

TODO.md

@@ -1,5 +1,7 @@
-`equivalentInCtx` with `ctx.trail` handle recursive function
-`equivalentInCtx` call `applyOneStep`
+`same` and `sameInCtx` -- do not expend function with `definedName`
+
+`equalInCtx` with `ctx.trail` handle recursive function
+`equalInCtx` call `applyOneStep`
 
 `readback` handle recursive function
 

docs/diary/2025-06-21-the-right-way-to-handle-recursion.md

@@ -254,43 +254,46 @@ f3
 设计一个带有 solution 的 relation 作为 judgement：
 
 ```scheme
-(claim equivalent solution-t exp-t exp-t judgement-t)
+(claim equal solution-t exp-t exp-t judgement-t)
 ```
 
 先不定义推演规则，直接用命题的列表来写证明：
 
 ```scheme
-(equivalent
+(equal
+ []
+ f2 f3)
+(equal
  [(== f2 f3)]
  (F (F f2)) (F (F (F f3))))
-(equivalent
+(equal
  [(== f2 f3)]
  f2 (F f3))
-(equivalent
+(equal
  [(== f2 f3)
   (== f2 (F f3))]
  (F (F f2)) (F f3))
-(equivalent
+(equal
  [(== f2 f3)
   (== f2 (F f3))]
  (F f2) f3)
-(equivalent
+(equal
  [(== f2 f3)
   (== f2 (F f3))
   (== f3 (F f2))]
  (F f2) (F (F (F f3))))
-(equivalent
+(equal
  [(== f2 f3)
   (== f2 (F f3))
   (== f3 (F f2))]
  f2 (F (F f3)))
-(equivalent
+(equal
  [(== f2 f3)
   (== f2 (F f3))
   (== f3 (F f2))
   (== f2 (F (F f3)))]
  (F (F f2)) (F (F f3)))
-(equivalent
+(equal
  [(== f2 f3)
   (== f2 (F f3))
   (== f3 (F f2))
@@ -304,13 +307,13 @@ f3
 而是带有相位差的表达式相等呢？
 
 ```scheme
-(equivalent
+(equal
  []
  f2 (F f2))
-(equivalent
+(equal
  [(== f2 (F f2))]
  (F (F f2)) (F f2))
-(equivalent
+(equal
  [(== f2 (F f2))]
  (F f2) f2)
 ;; prove by lookup the substitution

src/lang/equivalent/Ctx.ts renamed to src/lang/equal/Ctx.ts

@@ -0,0 +1,7 @@
+import { type Value } from "../value/index.ts"
+import { emptyCtx } from "./Ctx.ts"
+import { equalInCtx } from "./equalInCtx.ts"
+
+export function equal(left: Value, right: Value): boolean {
+  return equalInCtx(emptyCtx(), left, right)
+}

src/lang/equal/equal.ts

@@ -5,38 +5,34 @@ import * as Values from "../value/index.ts"
 import { type Neutral, type Value } from "../value/index.ts"
 import { ctxUseName, type Ctx } from "./Ctx.ts"
 
-export function equivalentInCtx(ctx: Ctx, left: Value, right: Value): boolean {
+export function equalInCtx(ctx: Ctx, left: Value, right: Value): boolean {
   left = Values.lazyActiveDeep(left)
   right = Values.lazyActiveDeep(right)
 
   if (left.kind === "NotYet" && right.kind === "NotYet") {
-    return equivalentNeutralInCtx(ctx, left.neutral, right.neutral)
+    return equalNeutralInCtx(ctx, left.neutral, right.neutral)
   }
 
   if (left.kind === "Lambda" && right.kind === "Lambda") {
     const freshName = freshen(ctx.usedNames, left.name)
     ctx = ctxUseName(ctx, freshName)
     const v = Neutrals.Var(freshName)
     const arg = Values.NotYet(v)
-    return equivalentInCtx(ctx, apply(left, arg), apply(right, arg))
+    return equalInCtx(ctx, apply(left, arg), apply(right, arg))
   }
 
   return false
 }
 
-function equivalentNeutralInCtx(
-  ctx: Ctx,
-  left: Neutral,
-  right: Neutral,
-): boolean {
+function equalNeutralInCtx(ctx: Ctx, left: Neutral, right: Neutral): boolean {
   if (left.kind === "Var" && right.kind === "Var") {
     return right.name === left.name
   }
 
   if (left.kind === "Apply" && right.kind === "Apply") {
     return (
-      equivalentNeutralInCtx(ctx, left.target, right.target) &&
-      equivalentInCtx(ctx, left.arg, right.arg)
+      equalNeutralInCtx(ctx, left.target, right.target) &&
+      equalInCtx(ctx, left.arg, right.arg)
     )
   }
 

src/lang/equivalent/equivalentInCtx.ts renamed to src/lang/equal/equalInCtx.ts

@@ -0,0 +1 @@
+export * from "./equal.ts"

src/lang/equal/index.ts

@@ -1,6 +1,6 @@
 import dedent from "dedent"
 import { emptyEnv } from "../env/index.ts"
-import { equivalent } from "../equivalent/index.ts"
+import { equal } from "../equal/index.ts"
 import { evaluate } from "../evaluate/index.ts"
 import { type Exp } from "../exp/index.ts"
 import { formatExp } from "../format/formatExp.ts"
@@ -38,7 +38,7 @@ export function execute(mod: Mod, stmt: Stmt): null {
 function assertEqual(mod: Mod, left: Exp, right: Exp): void {
   const leftValue = evaluate(mod, emptyEnv(), left)
   const rightValue = evaluate(mod, emptyEnv(), right)
-  if (!equivalent(leftValue, rightValue)) {
+  if (!equal(leftValue, rightValue)) {
     throw new Error(dedent`
       [assertEqual] Fail to assert equal.
 
@@ -51,7 +51,7 @@ function assertEqual(mod: Mod, left: Exp, right: Exp): void {
 function assertNotEqual(mod: Mod, left: Exp, right: Exp): void {
   const leftValue = evaluate(mod, emptyEnv(), left)
   const rightValue = evaluate(mod, emptyEnv(), right)
-  if (equivalent(leftValue, rightValue)) {
+  if (equal(leftValue, rightValue)) {
     throw new Error(dedent`
       [assertNotEqual] Fail to assert NOT equal.