@ -12,17 +12,18 @@ This time you can make use of a [[http://bnfc.digitalgrammars.com/][BNFC]] speci
If you want to use Haskell then there is also a wrapper module ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]]) that exports the generated abstract syntax and some definitions that may be useful for testing your code ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.html][documentation]]). The wrapper module comes with a Cabal file ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/chi.cabal][~chi.cabal~]]) and a [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/cabal.project][~cabal.project~]] file that might make installation a little easier. Here is one way to (hopefully) get started:
If you want to use Haskell then there is also a wrapper module ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]]) that exports the generated abstract syntax and some definitions that may be useful for testing your code ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.html][documentation]]). The wrapper module comes with a Cabal file ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/chi.cabal][~chi.cabal~]]) and a [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/cabal.project][~cabal.project~]] file that might make installation a little easier. Here is one way to (hopefully) get started:
- Install all dependencies properly, including suitable versions of GHC and cabal-install ([[https://www.haskell.org/downloads/][installation instructions]]), as well as [[http://bnfc.digitalgrammars.com/][BNFC]].
+ Install all dependencies properly, including suitable versions of GHC and cabal-install ([[https://www.haskell.org/downloads/][installation instructions]]), as well as [[http://bnfc.digitalgrammars.com/][BNFC]].
- Put [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]], [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][~Chi.hs~]], [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/chi.cabal][~chi.cabal~]] and [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/cabal.project][~cabal.project~]] in an otherwise empty directory.
+Put [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]], [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][~Chi.hs~]], [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/chi.cabal][~chi.cabal~]] and [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/cabal.project][~cabal.project~]] in an otherwise empty directory.
- Run ~bnfc --haskell Chi.cf~ in that directory.
+ Run ~bnfc --haskell Chi.cf~ in that directory.
- Now it is hopefully possible to use standard ~cabal~ commands. You could for instance try the following (still in the same directory):
+Now it is hopefully possible to use standard ~cabal~ commands. You could for instance try the following (still in the same directory):
- First use cabal repl to start GHCi.
+ First use cabal repl to start GHCi.
- Then issue the following commands at the GHCi command prompt:
+Then issue the following commands at the GHCi command prompt:
#+begin_src haskell
#+begin_src haskell
importChi
importChi
importPrelude
importPrelude
pretty<$>(runDecode(decode=<<
pretty<$>
asDecoder(code=<<code(parse"\\x. x"))))
(runDecode(decode=<<asDecoder
(code=<<code(parse"\\x. x"))))
#+end_src
#+end_src
* Exercises
* Exercises
@ -49,7 +50,7 @@ rec foo = \m. \n. case m of
Give a high-level explanation of the mathematical function in $\mathbb{N} \rightarrow \mathbb{N} \rightarrow \text{Bool}$ that is implemented by this code.
Give a high-level explanation of the mathematical function in $\mathbb{N} \rightarrow \mathbb{N} \rightarrow \text{Bool}$ that is implemented by this code.
*** Answer
*** Answer
The function will check for equality of the two natural numbers. If they are both $Zero()$, then it returns true, and if both are the successor of a some values, it checks if they are equal. In the other cases, it returns false.
The function will check for equality of the two natural numbers. If they are both $\text{Zero}()$, then it returns true, and if both are the successor of a some values, it checks if they are equal. In the other cases, it returns false.
** (2p)
** (2p)
Consider the $\chi$ term /t/ with concrete syntax $C (\lambda z.z)$:
Consider the $\chi$ term /t/ with concrete syntax $C (\lambda z.z)$:
@ -78,13 +79,13 @@ If you use the BNFC specification above and Haskell, then the substitution funct
#+end_src
#+end_src
Test your implementation. Here are some test cases that must work:
Test your implementation. Here are some test cases that must work:
| ~x~ | $Z()$ | $\text{rec}\ x = x$| $\text{rec}\ x = x$ |
| ~y~ | $\lambda x.x$ | $\lambda x. (x y)$ | $\lambda x . (x (\lambda x . x))$ |
| ~y~ | $\lambda x.x$ | $\lambda x. (x y)$ | $\lambda x . (x (\lambda x . x))$ |
| ~z~ | $C(\lambda z . z)$ | $\text{case}\ z\ \text{of}\ \{ C(z) \rightarrow z \}$ | $\text{case}\ C(\lambda z. z) \ \text{of}\ \{ C(z) \rightarrow z \}$ |
| ~z~ | $C(\lambda z . z)$ | $\text{case}\ z\ \text{of}\ \{ C(z) \rightarrow z \}$ | $\text{case}\ C(\lambda z. z) \ \text{of}\ \{ C(z) \rightarrow z \}$ |
*** Answer
*** Answer
See Assignment.hs
See =Assignment.hs=.
** (1p)
** (1p)
Implement multiplication of natural numbers in $\chi$, using the representation of natural numbers given in the $\chi$ specification.
Implement multiplication of natural numbers in $\chi$, using the representation of natural numbers given in the $\chi$ specification.
@ -117,13 +118,13 @@ If you use the BNFC specification above and Haskell, then the interpreter should
Test your implementation, for instance by testing that addition (defined in the [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][wrapper module]]) works for some inputs. If addition doesn’t work when your code is tested, then your solution will not be accepted. Also make sure that the following examples are implemented correctly:
Test your implementation, for instance by testing that addition (defined in the [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][wrapper module]]) works for some inputs. If addition doesn’t work when your code is tested, then your solution will not be accepted. Also make sure that the following examples are implemented correctly:
- The following programs should fail to terminate:
- The following programs should fail to terminate:
- The following programs should terminate with specific results:
- The following programs should terminate with specific results:
+ The program $case C(D(),E()) of { C(x, x) \rightarrow x }$ should terminate with the value $E()$.
+ The program $case C(D(),E()) of { C(x, x) \rightarrow x }$ should terminate with the value $E()$.
+ The program $case C(\lambda x.x, Zero()) of { C(f, x) \rightarrow f x }$ should terminate with the value $Zero()$.
+ The program $case C(\lambda x.x, Zero()) of { C(f, x) \rightarrow f x }$ should terminate with the value $Zero()$.
@ -133,3 +134,4 @@ Test your implementation, for instance by testing that addition (defined in the
Note that implementing a call-by-value semantics properly in a language like Haskell, which is by default non-strict, can be tricky. However, you will not fail if the only problem with your implementation is that some programs that should fail to terminate instead terminate with a “reasonable” result.
Note that implementing a call-by-value semantics properly in a language like Haskell, which is by default non-strict, can be tricky. However, you will not fail if the only problem with your implementation is that some programs that should fail to terminate instead terminate with a “reasonable” result.
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.