Small changes to the values
This commit is contained in:
20
3or4/4.org
20
3or4/4.org
@ -27,6 +27,8 @@ Implement $\chi$ substitution as a $\chi$ program. You should construct a $\chi$
|
|||||||
\[ subst \ulcorner x \urcorner \ulcorner e \urcorner \ulcorner e' \urcorner \Downarrow \ulcorner e' [ x \leftarrow e] \urcorner \]
|
\[ subst \ulcorner x \urcorner \ulcorner e \urcorner \ulcorner e' \urcorner \Downarrow \ulcorner e' [ x \leftarrow e] \urcorner \]
|
||||||
|
|
||||||
You do not need to prove formally that this property is satisfied, but please test your code. You can for instance test that this implementation of substitution matches the one from the last assignment. The [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][wrapper module]] ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.html][documentation]]) contains some testing procedures, as well as routines for representing natural numbers and $\chi$ abstract syntax as constructor trees.
|
You do not need to prove formally that this property is satisfied, but please test your code. You can for instance test that this implementation of substitution matches the one from the last assignment. The [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][wrapper module]] ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.html][documentation]]) contains some testing procedures, as well as routines for representing natural numbers and $\chi$ abstract syntax as constructor trees.
|
||||||
|
** Answer
|
||||||
|
See =Self.hs=
|
||||||
|
|
||||||
* (2p)
|
* (2p)
|
||||||
Implement a $\chi$ self-interpreter. You should construct a $\chi$ expression, let us call it /eval/, that satisfies the following properties:
|
Implement a $\chi$ self-interpreter. You should construct a $\chi$ expression, let us call it /eval/, that satisfies the following properties:
|
||||||
@ -36,17 +38,19 @@ Implement a $\chi$ self-interpreter. You should construct a $\chi$ expression, l
|
|||||||
You do not need to prove formally that these properties are satisfied, but please test your code. Make sure that the following examples are implemented correctly:
|
You do not need to prove formally that these properties are satisfied, but please test your code. Make sure that the following examples are implemented correctly:
|
||||||
- The program $\text{eval}\ \ulcorner e \urcorner$ should fail to terminate when e is any of the following programs:
|
- The program $\text{eval}\ \ulcorner e \urcorner$ should fail to terminate when e is any of the following programs:
|
||||||
+ $\text{C}()\ \text{C}()$
|
+ $\text{C}()\ \text{C}()$
|
||||||
+ $\text{case}\ \lambda x.x\ \text{of}\ {}$
|
+ $\text{case}\ \lambda x.x\ \text{of}\ \{\}$
|
||||||
+ $\text{case}\ \text{C}()\ \text{of}\ { \text{C}(x) \rightarrow \text{C}() }$
|
+ $\text{case}\ \text{C}()\ \text{of}\ \{ \text{C}(x) \rightarrow \text{C}() \}$
|
||||||
+ $\text{case}\ \text{C}(\text{C}())\ \text{of}\ { \text{C}() \rightarrow \text{C}() }$
|
+ $\text{case}\ \text{C}(\text{C}())\ \text{of}\ \{ \text{C}() \rightarrow \text{C}() \}$
|
||||||
+ $\text{case}\ \text{C}(\text{C}())\ \text{of}\ { \text{C}() \rightarrow \text{C}(); \text{C}(x) \rightarrow x }$
|
+ $\text{case}\ \text{C}(\text{C}())\ \text{of}\ \{ \text{C}() \rightarrow \text{C}(); \text{C}(x) \rightarrow x \}$
|
||||||
+ $\text{case} \text{C}()\ \text{of}\ { \text{D}() \rightarrow \text{D}() }$
|
+ $\text{case}\ \text{C}()\ \text{of}\ \{ \text{D}() \rightarrow \text{D}() \}$
|
||||||
+ $(\lambda x.\lambda y.x) (\text{rec}\ x = x)$
|
+ $(\lambda x.\lambda y.x) (\text{rec}\ x = x)$
|
||||||
|
|
||||||
- The following programs should terminate with specific results:
|
- The following programs should terminate with specific results:
|
||||||
+ The program $\text{eval}\ \ulcorner case C(D(),E()) of { C(x, x) \rightarrow x } \urcorner$ should terminate with the value $\ulcorner E() \urcorner$.
|
+ The program $\text{eval}\ \ulcorner \text{case}\ C(D(),E())\ \text{of}\ \{ C(x, x) \rightarrow x \} \urcorner$ should terminate with the value $\ulcorner E() \urcorner$.
|
||||||
+ The program $\text{eval}\ \ulcorner case C(\lambda x.x, Zero()) of { C(f, x) \rightarrow f x } \urcorner$ should terminate with the value $\ulcorner Zero() \urcorner$.
|
+ The program $\text{eval}\ \ulcorner \text{case}\ C(\lambda x.x, Zero())\ \text{of}\ \{ C(f, x) \rightarrow f x \} \urcorner$ should terminate with the value $\ulcorner Zero() \urcorner$.
|
||||||
+ The program $\text{eval}\ \ulcorner case (\lambda x.x) C() of { C() \rightarrow C() } \urcorner$ should terminate with the value $\ulcorner C() \urcorner$.
|
+ The program $\text{eval}\ \ulcorner \text{case}\ (\lambda x.x) C()\ \text{of}\ \{ C() \rightarrow C() \} \urcorner$ should terminate with the value $\ulcorner C() \urcorner$.
|
||||||
+ The program $\text{eval}\ \ulcorner ((\lambda x.x)(\lambda x.x))(\lambda x.x) \urcorner$ should terminate with the value $\ulcorner \lambda x.x \urcorner$.
|
+ The program $\text{eval}\ \ulcorner ((\lambda x.x)(\lambda x.x))(\lambda x.x) \urcorner$ should terminate with the value $\ulcorner \lambda x.x \urcorner$.
|
||||||
|
|
||||||
For full credit your implementation must evaluate addition of natural numbers correctly, i.e. $\text{eval} \ulcorner \text{add}\ \ulcorner m \urcorner \ \ulcorner n \urcorner \urcorner$ must terminate with the value $\ulcorner \ulcorner m + n \urcorner \urcorner$, for arbitrary (small) $m, n \in \mathbb{N}$ (where add is an implementation of addition). The wrapper module contains some testing procedures that you can use.
|
For full credit your implementation must evaluate addition of natural numbers correctly, i.e. $\text{eval} \ulcorner \text{add}\ \ulcorner m \urcorner \ \ulcorner n \urcorner \urcorner$ must terminate with the value $\ulcorner \ulcorner m + n \urcorner \urcorner$, for arbitrary (small) $m, n \in \mathbb{N}$ (where add is an implementation of addition). The wrapper module contains some testing procedures that you can use.
|
||||||
|
** Answer
|
||||||
|
See =Self.hs=
|
||||||
|
|||||||
Reference in New Issue
Block a user