Bagaimana cara mendefinisikan suatu fungsi secara induktif pada dua argumen dalam Coq?

Bagaimana saya bisa meyakinkan Coq bahwa fungsi rekursif yang diberikan di bawah ini berakhir? Fungsi ini mengambil dua argumen induktif. Secara intuitif, rekursi berakhir karena salah satu argumen terurai.

Secara khusus, fungsi mengambil dua pohon sebagai input.

Inductive Tree :=
| Tip: Tree
| Bin: Tree -> Tree -> Tree.

Di Pohon, saya suka melakukan gaya induksi berikut.

Inductive TreePair :=
| TipTip : TreePair
| TipBin : Tree -> Tree -> TreePair
| BinTip : Tree -> Tree -> TreePair
| BinBin : TreePair -> TreePair -> TreePair.

Fixpoint pair (l r: Tree): TreePair :=
  match l with
    | Tip =>
      match r with
        | Tip => TipTip
        | Bin rl rr => TipBin rl rr
      end
    | Bin ll lr =>
      match r with
        | Tip => BinTip ll lr
        | Bin rl rr => BinBin (pair l rl) (pair lr r)
      end
  end.

Definisi TreePair diterima, tetapi definisi dari pasangan fungsi menghasilkan pesan kesalahan:

Error: Cannot guess decreasing argument of fix.

Jadi saya tertarik pada cara meyakinkan Coq tentang penghentian.

Definisi fixpoint Coq mengharuskan panggilan induktif menerima argumen yang lebih kecil secara struktural. Jauh di lubuk hati, konstruk fixpoint mengambil satu argumen: tidak ada konsep definisi rekursif bawaan atas dua argumen. Untungnya, definisi Coq tentang struktur yang lebih kecil mencakup tipe orde tinggi, yang sangat kuat.

Definisi fixpoint dua argumen Anda mengikuti pola sederhana: argumen pertama menjadi lebih kecil, atau argumen pertama tetap identik dan argumen kedua menjadi lebih kecil. Pola yang cukup umum ini dapat ditangani dengan fix-in-fix yang sederhana.

Fixpoint pair l := fix pair1 (r : Tree) :=
  match l with
    | Tip => match r with
              | Tip => TipTip
              | Bin rl rr => TipBin rl rr
            end
    | Bin ll lr => match r with
                    | Tip => BinTip ll lr
                    | Bin rl rr => BinBin (pair1 rl) (pair lr r)
                   end
  end.

Untuk kasus yang lebih kompleks, atau jika selera Anda berjalan seperti itu, Anda dapat menggunakan rekursi lebih dekat dengan cara yang diajarkan dalam kursus matematika, membangun titik tetap dari perhitungan langkah dan argumen berdasar yang terpisah , sering menggunakan ukuran bilangan bulat . Anda juga dapat membuat definisi Anda lebih terlihat seperti program klasik dalam bahasa non-total dengan penghentian terpisah menggunakan Programbahasa sehari - hari .