Polimorfisme dan tipe data induktif

Saya penasaran. Saya telah mengerjakan tipe data ini di OCaml :

type 'a exptree =
  | Epsilon
  | Delta of 'a exptree * 'a exptree
  | Omicron of 'a
  | Iota of 'a exptree exptree

Yang dapat dimanipulasi menggunakan fungsi rekursif yang diketik secara eksplisit (fitur yang telah ditambahkan baru-baru ini). Contoh:

let rec map : 'a 'b. ('a -> 'b) -> 'a exptree -> 'b exptree =
  fun f ->
    begin function
    | Epsilon -> Epsilon
    | Delta (t1, t2) -> Delta (map f t1, map f t2)
    | Omicron t -> Omicron (f t)
    | Iota tt -> Iota (map (map f) tt)
    end

Tapi saya tidak pernah bisa mendefinisikannya dalam Coq :

Inductive exptree a :=
  | epsilon : exptree a
  | delta : exptree a -> exptree a -> exptree a
  | omicron : a -> exptree a
  | iota : exptree (exptree a) -> exptree a
.

Coq merengek. Itu tidak suka konstruktor terakhir, dan mengatakan sesuatu yang saya tidak sepenuhnya mengerti atau setuju dengan:

Error: Non strictly positive occurrence of "exptree" in "exptree (exptree a) -> exptree a".

Apa yang bisa saya pahami adalah bahwa tipe induktif yang menggunakan negasi di dalam definisi mereka seperti type 'a term = Constructor ('a term -> …)ditolak, karena mereka akan mengarah pada binatang buas yang jelek seperti (tanpa huruf) terms istilah. Namun exptreetipe data ini tampaknya cukup berbahaya: melihat definisi OCaml -nya, argumennya 'atidak pernah digunakan dalam posisi negatif.

Tampaknya Coq terlalu berhati-hati di sini. Jadi apakah benar-benar ada masalah dengan tipe data induktif khusus ini? Atau bisakah Coq sedikit lebih permisif di sini?

Juga, bagaimana dengan asisten bukti lainnya, apakah mereka mampu mengatasi definisi induktif semacam itu (dengan cara alami)?

Ini telah muncul di milis Coq beberapa kali, tetapi saya tidak pernah melihat jawaban konklusif. Coq tidak seumum mungkin; aturan dalam (Coquand, 1990) dan (Giménez, 1998) (dan tesis PhD-nya) lebih umum dan tidak memerlukan kepositifan yang ketat. Namun, kepositifan tidak cukup, ketika Anda pergi keluar Set; contoh ini muncul dalam beberapa diskusi :

Inductive Big : Type := B : ((B -> Prop) -> Prop) -> Big.

Dengan struktur data sederhana seperti milik Anda, tipe induktif tidak akan menimbulkan masalah selain membuat implementasi lebih kompleks.

Ada cara umum untuk mendefinisikan tipe seperti ini yang didefinisikan sebagai titik tetap polinomial:

$$F = \epsilon + \delta\, (F \times F) + \omicron\, \mathrm{id} + F \circ F$$

Alih-alih mencoba mendefinisikan fungsi , tentukan keluarga jenis . Ini berarti menambahkan parameter integer ke tipe yang mengkodekan jumlah komposisi mandiri ( , , , dll), dan konstruktor injeksi tambahan untuk mengubah menjadi .$\mathrm{exptree} : a \mapsto \mathrm{exptree}(a)$$\mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree} \circ \mathrm{exptree}, \ldots$$\mathrm{exptree}^0(a) = a$$\mathrm{exptree}^1(a) = \mathrm{exptree}(a)$a e x p t r e e 0 ( a ) = $\mathrm{exptree}^2(a) = \mathrm{exptree}(\mathrm{exptree}(a))$$a$$\mathrm{exptree}^0(a) = a$

Inductive et : nat -> Type -> Type :=
  | alpha : forall a, a -> et 0 a                      (*injection*)
  | omicron : forall n a, et n a -> et (S n) a         (**)
  | epsilon : forall (S n) a, et (S n) a
  | delta : forall n a, et (S n) a -> et (S n) a -> et (S n) a
  | iota : forall n a, et (S (S n)) a -> et (S n) a
.

Anda dapat melanjutkan untuk menentukan nilai dan mengerjakannya. Coq akan sering dapat menyimpulkan eksponen. Set Implicit Argumentsakan membuat definisi ini lebih cantik.

Definition exptree := et 1.
Definition et1 : exptree nat :=
  delta _ _ (omicron _ _ (alpha _ 42)) (epsilon _ _).
Definition et2 : exptree nat := iota _ _ (omicron _ _ et1).

Anda dapat memilih untuk menurunkan argumen dengan 1, sehingga exptreeadalah et 0. Ini menghilangkan banyak S ndalam definisi, yang dapat membuat beberapa bukti lebih mudah, tetapi membutuhkan pemisahan kasus awal dari kasus perulangan di setiap konstruktor yang mengambil dalam argumen (alih-alih menambahkan konstruktor injeksi tunggal untuk ). Dalam contoh ini, hanya ada satu konstruktor untuk dipisah, jadi ini harus menjadi pilihan yang baik.$a$$a$

Inductive et : nat -> Type -> Type :=
  | omicron_0 : forall a, a -> et 0 a
  | omicron_S : forall n a, et n a -> et (S n) a
  | epsilon : forall n a, et n a
  | delta : forall n a, et n a -> et n a -> et n a
  | iota : forall n a, et (S n) a -> et n a
.
Definition exptree := et 0.
Definition et1 : exptree nat :=
  delta _ _ (omicron_0 _ 42) (epsilon _ _).
Definition et2 : exptree nat :=
  (iota _ _ (omicron_S _ _ et1)).

Saya pikir ini adalah prinsip yang sama yang diusulkan dalam bentuk yang lebih umum oleh Ralph Mattes .

Referensi

Thierry Coquand dan Christine Paulin. Jenis yang ditentukan secara induktif . Dalam Proceedings of COLOG'88 , LNCS 417, 1990. [ Springer ] [ Google ]

Eduardo Giménez. Definisi Rekursif Struktural dalam Teori Tipe . Dalam ICALP'98: Prosiding Kolokium Internasional ke 25 tentang Automata, Bahasa dan Pemrograman. Springer-Verlag, 1998. [ PDF ]

Ralph Matthes menjelaskan cara mensimulasikan tipe seperti ini dalam Coq dalam "A Datastructure for Iterated Powers" ( kode , kertas ).

Salah satu hal pertama yang dilakukan Coq adalah membangun prinsip induksi yang terkait dengan tipe induktif yang baru saja Anda tentukan dan memahami prinsip induksi yang mendasarinya adalah latihan yang baik.

Misalnya O : nat | S : nat -> natakan menghasilkan prinsip induksi P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n.

Apa yang akan sesuai dengan prinsip induksi iota? Tampaknya tidak ada predikat Pyang akan mampu untuk berbicara tentang P tdan P (iota t), karena itu harus berbicara tentang exptree a, exptree (exptree a), exptree (exptree (exptree a))...

Juga Omicronmelakukan hal yang sama tetapi tipenya lebih kecil setiap kali. Anda harus merasa bahwa memiliki referensi untuk tipe yang lebih kecil dan tipe yang lebih besar akan membuat segalanya berantakan. (Konon, Omicronitu jalan yang benar)

Itu bukan kriteria tepat yang mengatakan mengapa definisi itu tidak boleh diterima tetapi ini menjelaskan mengapa itu terasa salah bagi saya.

exptreeSepertinya Anda sedang membangun sebuah tata bahasa untuk ekspresi, hal yang umumnya tidak yang rekursif. Apakah Anda ingin bantuan dengan itu?