Email Gateway (Aug 18 2022 at 11:43): Email Gateway (Aug 18 2022 at 11:43):From: TIMOTHY KREMANN <twksoa262@verizon.net>
Cheers,
Has someone compiled answers to the Tutorial's exercises? I am particularly having trouble with 3.4.1
Here is what I have so far? Am I getting close?
primrec
"norma (IF b a1 a2) = normifb (normb b) (norma a1) (norma a2)"
"norma (Sum a1 a2) = Sum (norma a1) (norma a2)"
"norma (Diff a1 a2) = Diff (norma a1) (norma a2)"
"norma (Var v) = Var v"
"norma (Num n) = Num n"
"normb (Less a1 a2) = Less (norma a1) (norma a2)"
"normb (And b1 b2) = And (normb b1) (normb b2)"
"normb (Neg b) = Neg (normb b)"
primrec
"normifa (IF b a1 a2) = (normifb b (normifa a1) (normifa a2))"
"normifa (Sum a1 a2) = Sum (normifa a1) (normifa a2)"
"normifa (Diff a1 a2) = Diff (normifa a1) (normifa a2)"
"normifa (Var v) = Var v"
"normifa (Num n) = Num n"
"normifb (Less a1 a2) t e = IF (Less (normifa a1) (normifa a2)) t e"
"normifb (And b1 b2) t e = (normifb b1 (normifb b2 t e) e)"
"normifb (Neg b) t e = (normifb b e t)"
Email Gateway (Aug 18 2022 at 11:44):From: Tobias Nipkow <nipkow@in.tum.de>
My solution looks very similar, but I have managed to fold your two
norma and normb functions into 1 function each. Hence I cannot say for
sure if your proposal is correct. But as I said, basically it looks good.
Tobias
TIMOTHY KREMANN wrote:
Last updated: May 03 2024 at 04:19 UTC