表示λ项的β相等类型的正确方法是什么？

Question

我正在寻找一个BetaEq类型索引a : Term，b : Term，如果a和b是相同的，或者如果它们可以在一系列beta减少后变成相同的术语。例如，假设id = (lam (var 0))，a = (app id (app id id))和b = (app (app id id) id);那么我们应该能够构建一个BetaEq a b类型的术语，因为双方都可以缩减为(app id id)。我试过这个：

data BetaEq : (a : Term) -> (b : Term) -> Set where
  refl : (a : Term) -> BetaEq a a
  redl : (a : Term) -> (b : Term) -> BetaEq (apply-redex a) b -> BetaEq a b
  redr : (a : Term) -> (b : Term) -> BetaEq a (apply-redex b) -> BetaEq a b

apply-redex执行单一减少的地方。但这看起来有点发明，所以我不确定这是否是正确的方法。请注意，这两个术语可能存在分歧，因此我们不能简单地考虑正常形式。代表beta-equality的标准方法是什么？

Answer 1

假设范围广泛的无类型lambda术语：

open import Data.Fin
open import Data.Nat

data Tm (n : ℕ) : Set where
  var : Fin n → Tm n
  app : Tm n → Tm n → Tm n
  lam : Tm (suc n) → Tm n

还有最外层变量的单个替换的定义（但请注意，在并行替换方面定义单个替换总是更可取的）：

sub : ∀ {n} → Tm n → Tm (suc n) → Tm n

然后beta等式是beta减少的同余关闭：

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''

通过同余闭包，我们的意思是最小的关系：

• 等价关系，即自反，对称和传递的关系。
• 与术语构造函数的一致性，即减少可以在任何构造函数内部发生。
• 通过一步式beta减少暗示。

或者，您可以给出一个有针对性的减少概念，然后将可转换性定义为减少到一个常用术语：

open import Data.Product
open import Relation.Binary.Closure.ReflexiveTransitive

-- one-step reduction
data _~>_ {n} : Tm n → Tm n → Set where
  β    : ∀ {t u} → app (lam t) u ~> sub u t
  app₁ : ∀ {t t' u} → t ~> t' → app t u ~> app t' u
  app₂ : ∀ {t u u'} → u ~> u' → app t u ~> app t u'
  lam  : ∀ {t t'} → t ~> t' → lam t ~> lam t'

-- multi-step reduction as reflexive-transitive closure
_~>*_ : ∀ {n} → Tm n → Tm n → Set
_~>*_ = Star _~>_

_~_ : ∀ {n} → Tm n → Tm n → Set
t ~ u = ∃ λ t' → (t ~>* t') × (u ~>* t')

这取决于版本更方便的情况。情况是两个定义是等价的，但AFAIK证明这种等价是相当困难的，因为它需要显示减少的confluence。