正確には「大規模排除」とは何ですか?

私はタイプ理論(主にCoq)を勉強しており、通常、タイプのユニバース階層の一貫性について言及するとき、「大規模な消去」という用語によく遭遇します。

impredicative polymorphism + excluded middle + large elimination
=> false

私はそれが意味するものを直感的に理解していますが、正確に何が「大規模な排除」であるかのより正式な定義を見つけたり構築したりすることはできませんでした。

私の理解では、 D の値を得るために t:T という用語を削除(破壊)
em> t の値に依存します。

For example, if vec_bool : nat -> Type is a type
constructor for the boolean list of a fixed size with data
constructors

nil  : vec_bool 0
cons : forall n:nat, bool -> vec_bool n -> vec_bool (S n)

次の再帰的定義は n で大幅に削除されます。

Fixpoint construct_false_list (n:nat) : vec_bool n :=
   match n with
   | 0      => nil
   | Succ m => cons m false (construct_false_list m)
   end.

私の理解は正しいのですか?何か不足していますか?

ベストアンサー

大きな除外の定義については間違っています。帰納的価値を排除することによって$ mathrm {Type}
$型のを構築する能力を指します。標準的な例:

bool_to_type : bool -> Type := fun b =>
     match b with
         | true => Unit
         | false => Empty

UnitEmpty
はそれぞれコンストラクタが1つと0の誘導型です。特に、これにより命題$ 0 not = 1
$を証明することができますが、これはこの能力がないと証明できません。

As noted in another answer (https://cstheory.stackexchange.com/a/21878/3984)
a good resource that explains this is the following github repo:
https://github.com/FStarLang/FStar/issues/360

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です