2

以下が機能するのはなぜですか：

fun f :: "nat ⇒ bool" where
  "f _ = (True ∨ (∀x. x))"

しかし、これは失敗します

fun g :: "nat ⇒ bool" where
  "g _ = (True ∨ (∀a. True))"

と

Additional type variable(s) in specification of "g_graph": 'a 
Specification depends on extra type variables: "'a"
The error(s) above occurred in "test.g_sumC_def"
The error(s) above occurred in definition "g_sumC_def":
  "g_sumC ≡ λx. THE_default undefined (g_graph TYPE('a) x)"

同様に、以下は成功します。

value "True ∨ (∀x. x)"

しかし、これは失敗します

value "True ∨ (∀x. True)"

と

Wellsortedness error:
Type 'a not of sort enum
Cannot derive subsort relation {} < enum
4

2 に答える 2

3

簡単な答えは次のとおりです。最初の関数定義では、型推論はそれxが型boolであると簡単に推測しますが、2番目の定義では、バインドされた変数aは他の場所では使用されないため、その型は任意です( 'a)。仕様の追加の型変数 ...が表現するものはどれですか。

の型を明示的に制約する場合a、たとえば、

fun g :: "nat ⇒ bool" where
  "g _ = (True ∨ (∀a::bool. True))"

関数定義が受け入れられます。

より長い答え:の定義は再帰的ではないため、 の代わりにgusing に変えることができます。最初の試みは完全に失敗するわけではありませんが、その結果に驚くかもしれません。後definitionfun

definition g :: "nat ⇒ bool" where
  "g _ = (True ∨ (∀a. True))"

の型はg、'a itself => nat => bool意図した の代わりにnat => boolです。fun理由は前回の失敗と同じです。は任意の型であるためa、この追加の型は の型に記録する必要がありますg。これは、この追加の型を明示的に示す追加の仮引数を導入することによって行われます。これは、型を引数として取る'a itselfコンストラクターによって、用語レベルで型情報をエンコードできる型です。例えば、TYPE(...)

TYPE('a)   :: 'a itself
TYPE(bool) :: bool itself
TYPE(nat)  :: nat itself

次に、 whereg TYPE(nat)のバージョンがタイプ に固定されます。ganat

あなたのvalueステートメントに関して、2番目のステートメントが失敗する理由は、実際には上記とは関係ありません。最初のステートメントでは、全称量指定子は、bool値を明示的に列挙できる型の変数をバインドするため、これらすべての値を考慮して結果を計算できます。対照的に、2 番目のステートメントでは、バインドされた変数は、値を明示的に列挙できないx任意の型です。'a

于 2013-09-16T03:08:42.640 に答える
1

以下は失敗します。

fun f where "f _ = (∀a. True)"

の型には多態性aが隠されている(つまり、関数の型シグネチャに存在しない型変数が関数の本体内にある) ため、関数パッケージの内部証明が混乱します。

明示的にa型を指定した場合:

fun f where "f _ = (∀a::bool. True)"

または、次のようaに、関数の型シグネチャにもある型を指定していますか?

fun f where "f _ = (∀a::bool. True)"

関数定義は成功します。あなたの例:

fun f where "f _ = (∀x. x)"

xは強制的に type になるため、成功しますbool。

コマンドに関してvalueは、Isabelle は式の実行可能コードを生成しようとするため、for-all ステートメントの型を知るだけでなく、可能な値をすべて列挙して、それらすべてをテストできるようにする必要があります。 . などのbool型は問題なく動作しますが、型変数'aや などの無限型natは列挙できないため、Isabelle はそれらのコードを生成できません。

于 2013-09-16T03:12:27.180 に答える