W-Typen vs Induktive Typen

Die Martin-Löf-Typentheorie verwendet W-Typen, um induktive Strukturen wie ganze Zahlen, Listen usw. zu definieren. Die Berechnung induktiver Konstruktionen verwendet sie jedoch nicht auf die gleiche Weise. Induktive Typen scheinen eher Axiomschemata zu sein.

Sind diese beiden Ansätze gleichwertig (sie scheinen es zu sein)? Gibt es philosophische Gründe, warum einer besser ist als der andere (für mich fühlen sich W-Typen intuitiver an, weil es sich nur um Bäume mit besonderer Struktur handelt)? Was aus Sicht der Implementierung einfacher ist (induktive Typen scheinen für mich besser zu sein, da für W-Typen mindestens endliche Typen und Produkte im Kern eines Systems verfügbar sein müssen, damit sie nützlich sind).

(Ich gehe davon aus, dass Sie mit 'Axiomschemata' an die Arbeit von Gimenez denken )

Im weiteren Sinne sind W-Typen und Gimenez 'Axiomschemata äquivalent.

In einer intensiven Umgebung werden Sie mit W-Typen jedoch nicht weit kommen: Sie sind zu umfangreich (gemäß der Definition der Codierung), um für die Programmierung geeignet zu sein. Dies wurde von mehreren Autoren diskutiert, insbesondere:

• Conor McBride: http://mazzo.li/epilogue/index.html%3Fp=324.html
• Peter Dybjer, "Darstellung induktiv definierter Mengen durch Wellordnungen in Martin-Löfs Typentheorie"
• Guogen & Luo, "Induktive Datentypen: übergeordnete Typen überarbeitet"