时间戳

首页 > 解决方案 > 表示 λ 项的 beta 等式类型的正确方法是什么？

agda - 表示 λ 项的 beta 等式类型的正确方法是什么？

问题描述

我正在寻找一种在 , 上被BetaEq索引的类型a : Term，b : Term它可以在当且仅当且仅当的情况下被居住，或者如果它们可以在一系列 beta-reductionsa后b变成相同的术语。例如，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

Whereapply-redex执行单个归约。但这看起来有点发明，所以我不确定这是否是正确的方法。请注意，这两个术语可能会有所不同，因此我们不能简单地考虑范式。表示 beta 等式的标准方法是什么？

标签： agda

解决方案

假设范围良好的无类型 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 证明这种等价性相当困难，因为它需要显示归约的汇合。

推荐阅读