Assignments PRF

Assignments PRF

This assignment has to be solved individually and handed in using the fire system before Monday 30 Nov.

This week you are going to implement (in Haskell or some other programming language) the set of primitive recursive functions in two ways. I want you to submit a file which can be compiled (and thus contains no syntactic errors).

    1. The first way is to implement the set of primitive recursive functions as the type [Int] -> Int and then the basic programs in PRF in the following way:

      1. type PRFs = [Int] -> Int zero :: PRFs suc :: PRFs proj :: Int -> PRFs compose :: PRFs -> [PRFs] -> PRFs rec :: PRFs -> PRFs -> PRFs zero = error "not implemented yet" suc = error "not implemented yet" proj = error "not implemented yet" compose = error "not implemented yet" rec = error "not implemented yet" add = rec (proj 0)(compose suc [proj 1]) pre = rec (zero) (proj 0) mul = error "not implemented yet" fact = rec (compose suc [zero]) (compose mul [compose suc [proj 0], proj 1])

    2. It is important that you give error messages when the length of the input list is erroneous, or when negative integers are used.

  1. The next implementation is to first implement a version of the abstract syntax as a data type PRF and then the denotational semantics which takes an object in PRF to a function in PRFs (as defined above). The abstract syntax of PRF (as given in the lecture notes) cannot immediately be defined in Haskell, since Haskell does not allow types depending on objects in other types. (The data type PRF(i) depends on the natural number i.) We therefore make the following simplification of the inductive definition of the abstract syntax:

    1. The set PRF is defined inductively by:

      1. Zero : PRF Succ : PRF Proj(i) : PRF if i: N Compose(g, fs): PRF if g: PRF, fs: List(PRF) Rec(g, h) : PRF if g, h: PRF

    2. Here, I have used colon (:) to denote membership in a set. Implement PRF as a data type in Haskell and implement then a function

      1. eval : PRF -> PRFs

    1. which is an implementation of the denotational semantics of PRF.