In this problem we set will represent some functional programs as data objects and manipulation them in various ways. The description of the functional programming language syntax is given in fp.mod. Various example functional programs are in the file fpexs.mod.
type infer exp -> ty -> o.that infers the type of expressions. If an expression is ill-typed then this predicate should fail. You should be able to reproduce the following session using the example programs in fpexs.mod.
type red1 exp -> exp -> o. type reduce exp -> exp -> o.where red1 relates two expressions if the second expression results from replacing exactly one rewriting redex somewhere within the first expression. The reduce relationship that repeatedly applies red1 until it cannot be applied further and returns the resulting expression. You should be able to reproduce the following session using the example programs in fpredex.mod.