0

Isabelle に次のコードがあります。

typedecl type1
typedecl type2

consts 
  A::"type1 set"
  B::"type2 set"

以下のように A と B でユニオン演算を使用したい場合:

axiomatization where
 c0: "A  ∩ B = {}"

A と B は異なる型のセットなので、型の衝突のエラーが発生します。これは理にかなっています!

暗黙的にオペランドを純粋なセットと見なす (つまり、その型を無視する) 集合演算に対応するものがあるかどうか疑問に思っています。したがって、 A ∩' B のようなものが可能になります ( ∩' は上記の意味での ∩ 演算の対応物です)。

PS：別の回避策は、質問をより適切に整理するために、ここで別の質問としてこれを書いた型キャストです。

ありがとう

4

1 に答える 1

3

Isabelle/HOL のセットは常に型付けされます。つまり、1 つの型の要素のみが含まれます。型なしセットが必要な場合は、Isabelle/ZF などの別のロジックに切り替える必要があります。

同様に、HOL のすべての値には型の注釈が付けられており、これはロジックの基本です。たとえば、等値は同じ型の 2 つの値にのみ適用できます。したがって、異なる型の値が等しいという概念はありません。したがって、値の型を無視する集合演算はありません。そのような演算は、異なる型の値を識別する方法を必ず知っている必要があるためです。

于 2014-11-11T12:41:27.373 に答える