CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion

David Wahlstedt (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Göteborg : Chalmers University of Technology, 2007. ISBN: 978-91-7291-979-2.- viii,120p s.

We present a variation of Martin-Löf's logical framework with "beta-iota-equality", extended with first-order parameterized algebraic data types and recursive pattern-matching definitions. Our contribution is a proof of normalization for the proposed system, from which we obtain decidable type-correctness. Our result holds under the assumption that the call relation of the recursive definitions is well-founded.

Recursive definitions can be read as intuitive specifications, which makes it easier to understand their intended meaning, compared to definitions that use only pre-defined recursion operators, called elimination rules in type theory. Pattern-matching definitions can be seen as the underlying mechanism with which we describe elimination rules. The arguments used to justify recursively defined elimination rules are essentially the same as those justifying pattern-matching definitions. The use of pattern-matching takes the proof system closer to the look and feel of a programming language like Haskell or ML.

We use the "Size-Change Principle for Program Termination" (C.S. Lee, N.D. Jones, A. Ben-Amram 2001) to establish that the recursive definitions have a well-founded call relation. The size-change criterion subsumes many known characterizations of terminating recursions, including primitive recursion and lexicographical ordering, but it also deals transparently with permuted arguments and mutual recursion. When instantiating the size-change relation for this criterion to be constructor decomposition, it corresponds closely to what we could call well-founded structural recursion.

Denna post skapades 2007-08-16. Senast ändrad 2013-09-25.
CPL Pubid: 45188


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)


Matematisk logik

Chalmers infrastruktur


Datum: 2007-09-14
Tid: 10.15
Lokal: Lecture room EA, ED&IT-building, Hörsalsvägen 11, Göteborg
Opponent: Chargé de Recherche HDR Ralph Matthes, IRIT -- Université Paul Sabatier, Toulouse, France

Ingår i serie

Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie 2660

Technical report D - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University 34D