校正時のη変換問題を避けるために、無駄な `id`呼び出しで変数を囲むのは普通ですか？

Question

Morte/CoCに似た言語を使って、簡単な文there are lists of arbitrary lengthsを証明しようとしています。

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

ThereIs依存ペア（シグマ）である。そのために、私は以下のタイプを書きました。すべて教会でコード化されています。それを証明するために、私は次の証明を書いた：変なふう

λ 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（タイプナットのすなわち、自由変数）とλ c:* -> λ b:(c -> c) -> λ a:c -> (d c b a)間の型の不一致エラーが発生します。しかし、それ以降の用語は、eta-reducedのときは、ちょうどdです！それはn、I「UN-ETA」のすべての出現にその役に立たないIDを適用することで、今

λ n: Nat -> 

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

(n Nat Succ Zero) 

：私はETA-減速の準備ができていないので、私が代わりにこれ以下の「無用の識別」機能を作りました証明を検証させます。私はここで何が起こっているのかについて何らかの洞察を得たいと思います。この "役に立たない"機能は、校正を書く上で知られている/使用されているパターンですか？なぜこのような助けを借りずに、この証明をタイプチェックすることができないのですか？この現象の背後に深い推論があるのでしょうか、それとも特別な理由がないかですか？

Answer 1

変換チェックアルゴリズムにηを追加する必要があります。すなわち、いくつかの方法で行うことができ、最も簡単な2つである

• タイプ指向Ulf Norell's thesisのページ22のように、使用Agda
に

コック私の知る限りで使用される型なし型なしETAの変換であります関数用に完全であり、型付きバージョンよりも簡単で高速です（中立アプリケーションで型を再計算またはキャッシュする必要はありません）。アルゴリズムは次のようになります。

まず、両方の値がいつものようにラムダである場合をチェックします。しかし、それ以降、2つの追加のケースをチェックします。片側のみがラムダです。このような場合、ラムダ本体を新しい汎用変数（通常どおり）に適用し、同じ変数にもう一方の項を適用し、結果の値の等価性をチェックします。

それはすべてです！実際には非常にシンプルで、パフォーマンスコストはあまりありません。 ηの変換チェックは弱いヘッドの通常の値で即座に実行されるため、ηの削減や強いηの正規化を実装する必要はありません。