Schema-guided inductive functional programming through automatic detection of type morphisms [Elektronische Ressource] / Martin Hofmann

Dissertationzur Erlangung des akademischen GradesDoktor der Naturwissenschaften (Dr.rer.nat.),eingereicht bei derFakultät Wirtschaftsinformatik und Angewandte Informatikder Otto-Friedrich-Universität BambergSchema-Guided Inductive FunctionalProgrammingthroughAutomatic Detection of Type MorphismsMartin HofmannOktober 2010Gutachter1. Gutachter: Prof.Dr.Ute Schmid (Universität Bamberg)2.hter: Prof.Dr.Petra Hofstedt (TU Cottbus)AbstractInductive functional programming systems can be characterised by two diametric ap-proaches: Either they apply exhaustive program enumeration which uses input/outputexamples (IO) as test cases, or they perform an analytical, data-driven structural gen-eralisation of the IO examples.EnumerativeapproachesignorethestructuralinformationprovidedwiththeIOexam-ples, but use type information to guide and restrict the search. They use higher-orderfunctions which capture recursion schemes during their enumeration, but apply themrandomly in a uninformed manner.Analytical approaches on the other side heavily exploit this structural information,but have ignored the benefits of a strong type system so far and use recursion schemesonly either fixed and built in, or selected by an expert user.In category theory universal constructs, such as natural transformations or type mor-phisms, describe recursion schemes which can be defined on any inductively defined datatype. They can be characterised by individual universal properties.