4

帰納的な定義でコンストラクターが使用できる入力の種類を何らかの形で制限したいと思います。次のように 2 進数を定義するとします。

Inductive bin : Type :=
  | O : bin
  | D : bin -> bin
  | S : bin -> bin.

ここでの考え方は、D は末尾にゼロを追加することでゼロ以外の数値を 2 倍にし、S は最後の桁としてゼロを含む数値を取り、最後の桁を 1 に変換するというものです。これは、以下が有効な数値であることを意味します。

S 0
D (S 0)
D (D (S 0))

次はそうではありません：

S (S 0)
D 0

帰納的な定義でそのような制限をクリーンな方法で強制する方法はありますか?

4

2 に答える 2

7

a が述語で正当であることの意味を定義し、その述語に従う sbinのサブセットに名前を付けることができます。bin次に、 and の代わりに and を使用して関数をProgram Definition記述Program FixpointしDefinitionますFixpoint。再帰関数の場合、関数は構造的に再帰的ではないため、関数の引数のサイズが減少することを証明する手段も必要です。

Require Import Coq.Program.Program.

Fixpoint Legal (b1 : bin) : Prop :=
  match b1 with
  | O       => True
  | D O     => False
  | D b2    => Legal b2
  | S (S _) => False
  | S b2    => Legal b2
  end.

Definition lbin : Type := {b1 : bin | Legal b1}.

Fixpoint to_un (b1 : bin) : nat :=
  match b1 with
  | O    => 0
  | D b2 => to_un b2 + to_un b2
  | S b2 => Coq.Init.Datatypes.S (to_un b2)
  end.

Program Definition zer (b1 : lbin) := O.

Program Fixpoint succ (b1 : lbin) {measure (to_un b1)} : lbin :=

しかし、この単純型付けのアプローチの方がおそらく簡単です。

于 2012-12-23T23:28:56.740 に答える
1

これは帰納的再帰定義で行うことができますが、残念ながら Coq はそれらをサポートしていません。

オブジェクト指向プログラミングの観点からするとO、DとSは のサブタイプでありbin、それらのコンストラクターの型は論理述語に頼らずに定義できますが、Coq はオブジェクト指向プログラミングもネイティブにはサポートしていません。

ただし、Coq には型クラスがあります。したがって、私ができることはbin、型クラスを作成し、各コンストラクターを個別の誘導型 (それぞれが型クラスのインスタンスを持つ) にすることbinです。ただし、型クラスのメソッドが何であるかはわかりません。

于 2012-12-23T10:12:07.443 に答える