25

Agdaでは、aのタイプはforall、次のすべてがタイプを持つように決定されますSet1（ここSet1で、はタイプであり、タイプSetはAタイプですSet）。

Set → A
A → Set
Set → Set

ただし、次のタイプは次のとおりSetです。

A → A

タイプがあった場合、矛盾が生じることは理解してSetいSetますが、上記の3つの用語のいずれかにタイプがあった場合、どのように矛盾が生じるかはわかりませSetん。それらを使用してFalseを証明できますか？それらを使用してそれを示すことができますSet : Setか？

4

2 に答える 2

18

ラッセルのパラドックスのSet : Setような矛盾を引き起こすことは明らかです。

ここで、ユニットタイプ() -> Setがどこにあるかを考えてみましょう。これは明らかに。と同型です。したがって、その場合も。実際、私たちが住んでいた人がいれば、定数関数を使用することになります。()Set() -> Set : SetSet : SetAA -> Set : SetSetA -> Set

wrap1 : {A : Set} -> Set -> (A -> Set)
wrap1 v = \_ -> v

必要に応じて値を取得します

unwrap1 : {A : Set}(anyInhabitant : A) -> (A -> Set) -> Set
unwrap1 anyInhabitant f = f anyInhabitant

したがって、ラッセルのパラドックスをあたかも持っているかのように再構築することができSet : Setます。

同じことが当てはまります。次のSet -> SetようにラップできSetますSet -> Set。

data Void : Set where

unwrap2 : (Set -> Set) -> Set
unwrap2 f = f Void

wrap2 : Set -> (Set -> Set)
wrap2 v = \_ -> v

ここでは、のSet代わりに任意のタイプを使用できますVoid。

と似たようなことをする方法はわかりませんSet -> Aが、直感的には、これは他のタイプよりもさらに問題のあるタイプのようです。おそらく他の誰かが知っているでしょう。

于 2012-09-23T13:13:01.470 に答える
7

これを理解する最良の方法は、Agdaではなく、集合論的集合としてこれらのものがどのようなものかを考えることだと思いますSet。あなたが持っているとしましょうA = {a,b,c}。関数の例はf : A → Aペアのセットです。たとえばf = { (a,a) , (b,b) , (c,c) }、この説明に関係のないいくつかのプロパティを満たしているとします。つまり、fの要素は、の要素と同じ種類のものAです。これらは単なる値、または値のペアであり、「大きすぎる」ものではありません。

ここで、関数について考えてみましょうF : A → Set。それもペアのセットですが、そのペアは異なって見えF = { (a,A) , (b,Nat) , (c,Bool) }ます。各ペアの最初の要素はの要素でAあるため、非常に単純ですが、各ペアの2番目の要素はSet！つまり、2番目の要素自体が「大きな」種類のものです。設定できなかった可能性があります。設定した場合は、のように見えるものを作成A → Setできるはずです。これができるとすぐに、ラッセルのパラドックスを得ることができます。代わりに言います。G : A → SetG = { (a,G) , ... }A → Set : Set1

これは、ペアのsが右側にあり、 sが左側にあることを除いて、の関数がの関数と同じであるため、の代わりにをSet → A含める必要があるかどうかの問題にも対処します。Set1SetSet → AA → SetASet

于 2012-09-25T21:17:29.070 に答える