60 lines
4.8 KiB
Org Mode
60 lines
4.8 KiB
Org Mode
#+title: Assignment 2
|
||
#+options: toc:nil
|
||
#+latex_header: \usepackage{parskip}
|
||
|
||
In order to pass this assignment you have to get at least three points. (Minor mistakes may be accepted.)
|
||
|
||
Please provide your source code in a form that 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.)
|
||
|
||
* (1p)
|
||
Give a brief explanation of the relationship between inductively defined sets, primitive recursion, and proofs by structural induction.
|
||
|
||
Here “primitive recursion” refers to the general concept, not the model of computation called PRF that is discussed in the course.
|
||
|
||
** Answer
|
||
Each inductively defined set has a number of constructors.
|
||
To prove something about these sets, the proposition needs to hold for the individual constructors, and the information that they hold.
|
||
In particular, if this definition is recursive in nature, one can depend that the recursion itself holds the proposition.
|
||
For natural numbers defined as $\mathbb{N} := \text{zero} | \text{succ}\ n$, that would look like $\text{P}\ \text{zero}\ \land (\forall n \in \mathbb{N}. \text{P}\ n \rightarrow \text{P}\ (\text{succ}\ n)) \rightarrow \forall n \in \mathbb{N}. \text{P}\ n$.
|
||
This proof on the structure is a generalized version of primitive recursion, which would have that $\text{P}$ be a function.
|
||
For natural numbers, that would be $A \land (\mathbb{N} \rightarrow A \rightarrow A) \rightarrow \mathbb{N} \rightarrow A$.
|
||
|
||
* (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 [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/reading/Some_mathematical_preliminaries.pdf][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, that every object that can be constructed corresponds to an integer, and that no two distinct objects correspond to the same integer.
|
||
|
||
/Hint/: Define the integers in terms of the natural numbers.
|
||
|
||
** Answer
|
||
See file attached.
|
||
* (1p) [BN]
|
||
[[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/reading/Some_mathematical_preliminaries.pdf][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.
|
||
|
||
If your inductive definition of the integers is not recursive (i.e. if the integers are not defined in terms of the integers), then zrec should not be recursive. Furthermore, if your inductive definition of the integers has n constructors, then there should be n cases in the implementation of zrec, one for each constructor.
|
||
|
||
Test that your function works. If it doesn’t, then you will not get full credit.
|
||
|
||
Note that if you define the integers in terms of another inductively defined set (like the natural numbers), then you can also use the higher-order recursion function for that set (like rec) when defining the successor function for the integers.
|
||
|
||
** Answer
|
||
See file attached.
|
||
* (2p) [BN]
|
||
The [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/lectures/L3.pdf][slides]] for the third lecture contain 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 /(n in PRF n)/, so you are allowed to omit them. If you do, implement the following inductive definition:
|
||
|
||
- $\text{zero} \in PRF$.
|
||
- $\text{suc} \in PRF$.
|
||
- $\text{proj}\ i \in PRF$ if $i \in \mathbb{N}$.
|
||
- $\text{comp}\ f\ gs \in PRF$ if $f \in PRF$ and $gs \in \text{List}\ PRF$.
|
||
- $\text{rec}\ f\ g \in PRF$ if $f, g \in 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 you will not get full credit.
|
||
** Answer
|
||
See file attached.
|