如何证明 Agda 中广义组合的伪结合性？

Question

我一直在尝试将论文“Continuation-Passing Style, Defunctionization, Accumulations, and Associativity”从 Idris 翻译为：https://arxiv.org/ftp/arxiv/papers/2111/2111.10413.pdf阿格达。

最后一个示例讨论了广义组合，它似乎等效于 Function.Nary.NonDependent.Base 中的

mapₙ

函数，并证明它是伪关联的。我一直在努力让它在 Agda 中进行类型检查。我想要的是如下类型：

mapₙ-assoc : ∀ {n m : ℕ} {ls ls′ r s t} {x : Set r} {y : Set s} {z : Set t} {as : Sets n ls} {bs : Sets m ls′}
  → (h : y → z) → (g : Arrows (suc m) (x , bs) y) → (f : Arrows n as x)
  → mapₙ n (mapₙ (suc m) h g) f ≡ mapₙ (n + m) h (mapₙ n g f)

但这不会类型检查错误：

n != n + m of type ℕ
when checking that the expression mapₙ n g f has type _as_1119 ⇉ y

我尝试过制作以下版本，但我不知道如何使归纳步骤起作用，或者即使它可以像这样工作。

mapₙ-assoc : ∀ {n m : ℕ} {ls ls′ r s t} {x : Set r} {y : Set s} {z : Set t} {as : Sets n ls} {bs : Sets m ls′}
  → (h : y → z) → (g : Arrows (suc m) (x , bs) y) → (f : Arrows n as x) → Set _
mapₙ-assoc {zero} {m} h g f = mapₙ zero (mapₙ (suc m) h g) f ≡ mapₙ (zero + m) h (mapₙ zero g f)
mapₙ-assoc {suc n} {m} h g f = {!!}

这个版本适用于我尝试过的任何特定的 n，而不仅仅是

zero

，所以我假设 Agda 可以扩展以查看类型是否相等，但我无法说服它它们具有通用的 n。

Answer 1

问题在于

mapₙ n g f

的类型为

Arrows n as (Arrows m bs y)

，而不是

Arrows (n + m) (as ++ bs) y

。您可以证明这些等价并在它们之间进行转换（您必须首先为

_++_

和

Levels

定义

Sets

），或者您可以只使用

mapₙ n (mapₙ m h)

而不是

mapₙ (n + m) h

。

mapₙ-assoc : ∀ {n m : ℕ} {ls ls′ r s t} {x : Set r} {y : Set s} {z : Set t} {as : Sets n ls} {bs : Sets m ls′}
  → (h : y → z) → (g : Arrows (suc m) (x , bs) y) → (f : Arrows n as x)
  → mapₙ n (mapₙ (suc m) h g) f ≡ mapₙ n (mapₙ m h) (mapₙ n g f)