是否通常将变量包装在无用的`id`调用中以避免证明上的eta转换问题？

Question

使用类似于Morte/CoC的语言,我试图证明这个简单的陈述there are lists of arbitrary lengths.为此,我写了以下类型:

? n:Nat ->
(ThereIs (List Nat)
  (Equal Nat 
    (List.length Nat l) 
    n)))

ThereIs是依赖对(Sigma).一切都是教会编码的.为证明这一点,我写了以下证据:

? n:Nat ->
(ThereIs.this (List Nat)
  (? l:(List Nat) -> (Equal Nat (List.length Nat l) n))
  (List.replicate Nat n Nat.Zero)
  (Equal.refl Nat n))

奇怪的是,我得到一个类型不匹配错误d(即Nat类型的自由变量)和? c:* -> ? b:(c -> c) -> ? a:c -> (d c b a).但是那个后期,当eta减少时,只是d!由于我没有准备好eta-reducer,我改为使用以下"无用识别"功能:

? n: Nat ->

? Nat:* ->
? Succ: (Nat -> Nat) ->
? Zero: Nat ->

(n Nat Succ Zero)

现在,通过将无用的id应用于每次出现n,我"un-eta"它,导致证据检查.我想对这里发生的事情有所了解.这个"无用的id"功能是在编写样张时已知/使用的模式吗？如果没有这么小的帮助,为什么结构的微积分能够输入 - 检查这个证明？这种现象背后是否存在任何深刻的推理,或者它是如何没有特殊原因的？

Answer 1

您需要将 eta 添加到您的转换检查算法中。这可以通过多种方式完成，最简单的两种是

在我们的例子中，非类型化 eta 转换对于函数来说是完整的，并且比类型化版本更简单、更快（不需要在中性应用程序中重新计算或缓存类型）。算法是这样的：

我们首先像往常一样检查两个值都是 lambda 的情况。然而，我们随后检查了另外两种情况，即只有一侧是 lambda 的情况。在这些情况下，我们将 lambda 主体应用于新的泛型变量（像往常一样），并将其他项应用于同一变量，并检查结果值的相等性。

这就是全部！其实很简单，并且没有太大的性能成本。请注意，我们不需要实现 eta 缩减或强 eta 归一化，因为 eta 转换检查很容易在运行时对弱头正常值进行。