Functional Programming

CAS 781, Winter 2003

Assignment 3

25. February 2003

Term Rewriting

Use the following data type for terms:

> data Term = Var String
>           | App String [Term]

Define the type FSymb appropriately, and functions
```
> vars   :: Term -> [String]
> fsymbs :: Term -> [FSymb]
```
mapping each term to the list of variable symbols (respectively function symbols) occurring in it.
Define a data type Subst for substitutions, and a function
```
> applySubst :: Subst -> Term -> Term
```
for applying substitutions to terms.
Define a function
```
> match :: Term -> Term -> Maybe Subst
```
such that the application ``match lhs t'' has the result ``Just s'' if and only if there is a substitution that, when applied to lhs, yields t; the s in the result then has to be that substitution.
For term rewriting rules, us the following data type:
```
> type Rule = (Term,Term)
```
Define a function
```
> applyRule :: Rule -> Term -> [Term]
```
that maps a rule r and a term t to all results of applying r te redexes in t.
Let the following data type for arbitrarily branching trees be defined:
```
> data Tree a = Tree a [Tree a]
```
Define a function
```
> derive :: [Rule] -> Term -> Tree Term
```
such that ``derive trs t0'' is the derivation tree of the term t0 in the term rewriting system trs.
Define a function
```
> nf :: [Rule] -> Term -> Term
```
that maps a term rewriting system trs and a term t0 always to a normal form of t0 in trs, if such a normal form exists.
Hint: Define an appropriate auxiliary function of type ``Tree a -> a''!
Define a function
```
> nf_deriv :: [Rule] -> Term -> [Term]
```
that, instead of the normal form found by nf, produces the whole derivation leading to that normal form.

A few rules for experiments:

> rPlus = [(App "+" [App "0" [], Var "x"], Var "x")
>         ,(App "+" [App "succ" [Var "x"], Var "y"]
>          ,App "succ" [App "+" [Var "x", Var "y"]])
>         ]

> rPcomm = (App "+" [Var "x", Var "y"], App "+" [Var "y", Var "x"])
> rPass1 = (App "+" [App "+" [Var "x", Var "y"], Var "z"]
>          ,App "+" [Var "x", App "+" [Var "y", Var "z"]])


> nat n = App (show n) []
> nsucc x = App "succ" [x]

> succrule n = (nat (succ n), nsucc (nat n))

> rn = map succrule [0..9]

> flop (x,y) = (y,x)
> rn'= map flop rn


> trs1 = rPcomm : rPlus ++ rn ++ [rPass1, flop rPass1]

> t1 = App "+" [App "3" [], App "1" []]

Nice test cases:

putStr $ unlines $ map show $ rn

nf trs1 t1

chop 3 $ derive trs1 t1

putStr $ unlines $ map show $ nf_deriv trs1 t1

nf rn' $ nf trs1 t1

Functional Programming - CAS 781, Winter 2003