PROGRAMMIERAUFGABE 4.1 datatype function = F of string; datatype term = V of string | @@ of function * term list; infix @@; exception nomatch; fun matchingSubst term term' = (* matchingSubstAccum: wie matchingSubst mit einem zusätzlichen Argument zum Aufsammeln der Substitution. *) let fun matchingSubstAccum (V s) term' accum = (s,term') :: accum | matchingSubstAccum (F(s)@@l) (F(s')@@l') accum = if s = s' then matchingSubstAccumList l l' accum else raise nomatch | matchingSubstAccum _ _ _ = raise nomatch (* matchingSubstAccumList: wie matchingSubstAccum für Termlisten anstelle von Termen. *) and matchingSubstAccumList [] [] accum = accum | matchingSubstAccumList [] _ _ = raise nomatch | matchingSubstAccumList _ [] _ = raise nomatch | matchingSubstAccumList (t::l) (t'::l') accum = matchingSubstAccumList l l' (matchingSubstAccum t t' accum) in matchingSubstAccum term term' [] end; PROGRAMMIERAUFGABE 4.2 fun applySubst subst (V s) = ( case List.find (fn (s',t') => s = s') subst of SOME (s',t') => t' | NONE => (V s) ) | applySubst subst (F(s)@@l) = F(s) @@ (map (applySubst subst) l); PROGRAMMIERAUFGABE 4.3 exception topirreducible; fun applyRulesOnceAtTop [] term = raise topirreducible | applyRulesOnceAtTop ((left,right)::l) term = applySubst (matchingSubst left term) right handle nomatch => applyRulesOnceAtTop l term; PROGRAMMIERAUFGABE 4.4 exception argsirreducible; exception irreducible; fun normalize rules term = let fun normalize' (term as (F(s)@@l)) = ( let val term1 = F(s)@@(normalizeList' l) in let val term2 = applyRulesOnceAtTop rules term1 in normalize rules term2 end handle topirreducible => term1 end handle argsirreducible => let val term2 = applyRulesOnceAtTop rules term in normalize rules term2 end handle topirreducible => raise irreducible ) | normalize' (term as (V s)) = ( let val term2 = applyRulesOnceAtTop rules term in normalize rules term2 end handle topirreducible => raise irreducible ) and normalizeList' [] = raise argsirreducible | normalizeList' (list as (term::rest)) = let val rest1 = normalizeList' rest in let val term1 = normalize' term in term1::rest1 end handle irreducible => term::rest1 end handle argsirreducible => let val term1 = normalize' term in term1::rest end handle irreducible => raise argsirreducible; in normalize' term handle irreducible => term end AUFGABE 4.5 Satz: Gegeben f und e so daß für alle x, y, z gilt: f(e,x) = x und f(x,f(y,z)) = f(f(x,y),z). Dann gilt für alle l und x: f(foldr f e l, x) = foldr f x l. Beweis: Strukturelle Induktion über l: Falls l = [], dann ist f(foldr f e [], x) = f(e,x) und foldr f x l = x nach Definition von foldr und f(e,x) = x nach Voraussetzung. Falls l = y::l', dann ist f(foldr f e (y::l'), x) = f(f(y, foldr f e l'), x) [nach Definition von foldr] = f(y, f(foldr f e l', x)) [wegen Assoziativität von f] = f(y, foldr f x l')) [nach Induktionsvoraussetzung] = foldr f x (y::l') [nach Definition von foldr]