Not logged in. · Lost password · Register

TMT
Member since Oct 2019
15 posts
Subject: Frage über (ko-)induktive Datentypen
In dem Skript zur Vorlesung wurde in Bezug auf induktive und koinduktive Datentypen der Begriff eines Mengenkonstruktors und einer Algebra eingeführt.

Was hat es denn hiermit genau auf sich? Insbesondere würde mich interessieren welche Rolle der Mengenkonstruktor in Bezug auf die Algebra spielt und wie man diesen für einen gegebenen koinduktiven Datentypen findet.

Vielen Dank im Vorraus für Antworten. : )
pwild
Member since Nov 2014
11 posts
Grundsätzlich sind die beiden Konzepte dual. Ein induktiver Datentyp ist die initiale F-Algebra FX -> X für eine Mengenkonstruktion F und ein koinduktiver Datentyp ist die terminale G-Koalgebra X -> GX für eine Mengenkonstruktion G.

Beispielsweise hat man beim induktiven Typ der Listen über einem Parametertyp A die Konstruktion FX = 1 + A*X. Die initiale F-Algebra ist dann List(A) mit der Abbildung 1 + A*List(A) -> List(A), und die Summanden in F entsprechen den Konstruktoren nil: 1 -> List(A) und cons: A*List(A) -> List(A).

Beim koinduktiven Typ der Streams über A ist die Konstruktion GX = A*X und Stream(A) ist die terminale G-Koalgebra mit der Abbildung Stream(A) -> A*Stream(A). Die Observer von Stream(A) entsprechen in diesem Fall den Faktoren in G, also hat man hd: Stream(A) -> A und tl: Stream(A) -> Stream(A).

Wenn man jetzt von den Konstruktoren eines gegebenen induktiven Typs oder den Observern eines gegebenen koinduktiven Typs auf die Mengenkonstruktion zurückschließen will, muss man die entsprechende Konstruktion umkehren, also bei einem induktiven Typ die Summe der linken Seiten oder bei einem koinduktiven Typ das Produkt der rechten Seiten bilden.
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen