[Club2] Mi. 25.01. 10.00Uhr,

[Norbert Schirmer]

++++++ ACHTUNG: Andere ZEIT, anderer RAUM !!!! +++++++

Diese Woche,

Mi. 25.01.06: 10.00 Uhr,  in Zuse (01.11.018),

Alexander Krauss:

Allgemeine Rekursion und partielle Funktionen
                 - "Recdef Next Generation" -


Dieser Vortrag beschreibt das neue Paket zur definitorischen Einf=FChrung=20
von rekursiven Funktionen in Isabelle/HOL.

Nach einer kurzen Einf=FChrung besprechen wir zun=E4chst einige=20
grunds=E4tzliche Schw=E4chen und Probleme des bisherigen Recdef-Pakets. Dan=
n=20
wird ein neues Verfahren vorgestellt, welches auf der induktiven=20
Definition des Graphen der Funktion, sowie einer "kleinsten=20
Terminierungsordnung" beruht. Man wird sehen, dass sich insbesondere=20
partielle und geschachtelt rekursive Funktionen auf diese Weise besser=20
behandeln lassen. Am Ende steht eine praktische Demonstration der=20
Implementierung.

   Norbert