Существует ли какая-либо связь между представлением бета-равенства в качестве его конгруэнтного замыкания и заменой подвыражения? - PullRequest
Новая
       9

Существует ли какая-либо связь между представлением бета-равенства в качестве его конгруэнтного замыкания и заменой подвыражения?

0 голосов
/ 01 марта 2019

Представление бета-равенства в Agda

Я недавно спросил , как правильно представлять бета-равенство на языке доказательства, таком как Agda.Принятый ответ указывает на стандартный способ сделать это путем определения его конгруэнтного замыкания 

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. рефлексивность, симметрия и транзитивность сохраняются.Ответ также предлагает альтернативу: можно определить одноэтапное редукционное отношение между терминами, затем определить многоэтапное редукционное отношение и, наконец, определить, что два термина равны, если их можно в конечном итоге уменьшить до идентичного термина.Обе эти альтернативы имеют смысл.

Другая альтернатива

Пока я ждал ответа, я искал это определение: 

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

Полный источник доступен здесь .Теперь, ради любопытства, я хотел бы знать, является ли третье решение также допустимым представлением?Если это так, каковы его отношения с двумя предыдущими?Если нет, то почему?

1 Ответ

0 голосов
/ 01 марта 2019

Небольшая проблема с этой попыткой заключается в том, что это соотношение не является согласованным: 

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

Поскольку мы можем использовать произвольную функцию Agda на b, тогда, пока у нас есть a, который уменьшается до b, мы можем разделить их в Agda и заменить произвольными / неравными значениями.Спасибо pgiarrusso на #agda в Freenode IRC за указание этого.

...