将β等式表示为同余闭包和子表达式替换之间是否存在任何关系？

Question

Representing beta-equality in Agda

我最近用像Agda这样的证明语言问what is the proper way to represent beta-equality。接受的答案指出一种标准的方法是通过定义其同余闭包，

data _~_ {n} : Tm n → Tm n → Set where
  β      : ∀ {t u} → app (lam t) u ~ sub u t
  app    : ∀ {t t' u u'} → t ~ t' → u ~ u' → app t u ~ app t' u'
  lam    : ∀ {t t'} → t ~ t' → lam t ~ lam t'
  ~refl  : ∀ {t} → t ~ t
  ~sym   : ∀ {t t'} → t ~ t' → t' ~ t
  ~trans : ∀ {t t' t''} → t ~ t' → t' ~ t'' → t ~ t''

如果我理解正确，则指定：1。应用程序(λx.t u)等于t[u/x]，2。应用程序的函数/参数或函数体可以用相等的术语替换; 3.反身性，对称性和传递性。答案还提出了另一种选择：人们可以定义术语之间的一步减少关系，然后定义多步骤减少关系，最后，如果最终可以减少到相同的术语，则定义两个术语相等。这两种选择都有意义。

Another alternative

当我在等待答案的时候，我正在看这个定义：

data _~_ : Term → Term → Set where
  refl : (a : Term) → a ~ a
  red₁ : (a b : Term) → (f : Term → Term) → f a ~ b → f (redex a) ~ b
  red₂ : (a b : Term) → (f : Term → Term) → a ~ f b → a ~ f (redex b)
  amp₁ : (a b : Term) → (f : Term → Term) → f (redex a) ~ b → f a ~ b
  amp₂ : (a b : Term) → (f : Term → Term) → a ~ f (redex b) → a ~ f b

如果redex a是λ应用，a应用单个替换。这表示如果术语相同，或者通过减少/减少其任何子表达式使术语相同，则术语是等效的。人们可以证明sym，trans，cong：

sym   : (a : Term) -> (b : Term) -> a ~ b -> b ~ a
trans : (a : Term) → (b : Term) → (c : Term) → a ~ b → b ~ c → a ~ c
cong  : (f : Term → Term) → (a : Term) → (b : Term) → a ~ b → f a ~ f b

完整的来源是here。现在，为了好奇，我想知道第三个解决方案是否也是一个有效的表示？如果是这样，它与前两个的关系是什么？如果没有，为什么？

Answer 1

这种尝试的一个小问题是这种关系是不一致的：

oops : var 0 ~ var 1
oops = red₂
  (var 0)
  (app id id)
  (λ { (lam typ (var 0)) -> var 1; t -> var 0 })
  (refl (var zero))

既然我们能够在b上使用任意的Agda函数，那么，只要我们有一个a减少到b，我们就能够在Agda中将它们分开并用任意/不等值替换它们。感谢在Freenode IRC #agda上的pgiarrusso指出这一点。