In order to pass this assignment you have to get at least three points. (Minor mistakes may be accepted.)
(1p) Give a brief explanation of the relationship between inductively defined sets, primitive recursion, and proofs by structural induction.
(1p) [BN] Define the integers inductively, implement this definition as a data type in a functional programming language (for instance Agda or Haskell), and show how the numbers -1, 0, 1 and 3 are represented using your definition. It should be easy to implement simple functions like addition and multiplication using your representation (but you don't have to do this).
Do not use the incorrect definition from Some mathematical preliminaries: sets, relations and functions. Be careful so that you avoid off-by-one errors. Make sure that every integer can be constructed using your definition, and that every object that can be constructed corresponds to a unique integer.
Hint: Define the integers in terms of the natural numbers.
(1p) [BN] Some mathematical preliminaries: sets, relations and functions mentions a higher-order function rec. Give the type of and implement an analogous function zrec for your definition of integers. Use this function to implement a function that adds one to an integer, without using pattern matching or recursion.
Test that your function works. If it doesn't, then your solution will not be accepted.
(2p) [BN] The primitive recursive functions contains an (indexed) inductive definition of the abstract syntax of the primitive recursive functions. Represent this definition as a data type in a functional programming language, show how one can encode addition of two natural numbers as a value in this type, and implement the denotational semantics of PRF as a function from your data type and a vector of natural numbers to a natural number.
Depending on what language you use it may be hard to handle the natural number indices (i in PRFᵢ), so you are allowed to omit them. If you do, implement the following inductive definition:
z ∈ PRF.
s ∈ PRF.
proj(i) ∈ PRF if i ∈ ℕ.
comp(g, fs) ∈ PRF if g ∈ PRF and fs ∈ List PRF.
rec(g, h) ∈ PRF if g, h ∈ PRF.
You are also allowed to represent fixed-length vectors by arbitrary-length vectors/lists, and to represent natural numbers using some kind of integer type. If you detect malformed input, then you can give an error message.
Test that addition works for some inputs. If it doesn't, then your solution will not be accepted.
Please provide your source code in a form which is easy to test, not, say, a PDF file.
(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.)