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

A Framework for Polytypic Programming on Terms, with an Application to Rewriting

Patrik Jansson (Institutionen för datavetenskap, Funktionell programmering ; Institutionen för datavetenskap, Programmeringslogik) ; Johan Jeuring
Workshop on Generic Programming (2000)
[Konferensbidrag, refereegranskat]

Rewriting is a typical example of a polytypic function. Given any value of a datatype (an algebra of terms), and rules to rewrite values of that datatype, we want a function that rewrites the value to normal form if the value is normalizable. This paper develops a polytypic rewriting function that uses the parallel innermost rewriting strategy. It improves upon our earlier work on polytypic rewriting in two fundamental ways. Firstly, the rewriting function uses a term interface that hides the polytypic part from the rest of the program. The term interface is a framework for polytypic programming on terms. This implies that the rewriting function is independent of the particular implementation of polytypism. We give several functions and laws on terms, which simplify calculating with programs. Secondly, the rewriting function is developed together with a correctness proof. We just present the result of the correctness proof, the proof itself is published elsewhere.



Denna post skapades 2006-10-09. Senast ändrad 2014-09-02.
CPL Pubid: 10126

 

Läs direkt!


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


Institutioner (Chalmers)

Institutionen för datavetenskap, Funktionell programmering (2002-2004)
Institutionen för datavetenskap, Programmeringslogik (2002-2004)

Ämnesområden

Teoretisk datalogi
Datalogi

Chalmers infrastruktur