Как правильно представлять тип бета-равенства для λ-членов? - PullRequest
Новая
       11

Как правильно представлять тип бета-равенства для λ-членов?

0 голосов
/ 28 февраля 2019

Я ищу тип BetaEq, индексированный по a : Term, b : Term, который может быть заселен, если a и 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

Где apply-redex выполняет одно сокращение.Но это выглядит немного придуманным, поэтому я не уверен, что это правильный способ сделать это.Обратите внимание, что оба термина могут расходиться, поэтому мы не можем просто рассмотреть нормальные формы.Каков стандартный способ представления бета-равенства?

1 Ответ

0 голосов
/ 28 февраля 2019

Предполагая, что нетипизированные лямбда-выражения хорошо ограничены: 

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

Тогда бета-равенство является конгруэнтным замыканием бета-редукции: 

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

Под конгруэнтным замыканием мы подразумеваем наименьшее отношение, которое равно:

  • Отношение эквивалентности, т. Е. Рефлексивное, симметричное и транзитивное.
  • Конгруэнция по отношению к конструкторам терминов, т.е. сокращение может иметь место внутри любого конструктора.
  • Подразумевается одноэтапным бета-редукцией,

В качестве альтернативы вы можете дать направленное понятие сокращения, а затем определить конвертируемость как сокращение к общему термину: 

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, доказывающий эту эквивалентность, довольно сложный, так как для этого требуется показать слияние сокращения.

...