From e749b82a8700507f7eff9213640d7d64a1d7cad3 Mon Sep 17 00:00:00 2001 From: pingu Date: Tue, 25 Nov 2025 17:29:31 +0100 Subject: [PATCH] Start on next --- {3 => 3or4}/.envrc | 0 {3 => 3or4}/.gitignore | 0 {3 => 3or4}/3.org | 0 3or4/4.org | 52 +++++++++++++++++++++++++++++++++ {3 => 3or4}/Chi.cf | 0 {3 => 3or4}/Chi.hs | 0 {3 => 3or4}/cabal.project | 0 {3 => 3or4}/chi.cabal | 1 + {3 => 3or4}/flake.lock | 0 {3 => 3or4}/flake.nix | 0 {3 => 3or4}/interpreter/Main.hs | 0 3or4/interpreter/Self.hs | 8 +++++ 12 files changed, 61 insertions(+) rename {3 => 3or4}/.envrc (100%) rename {3 => 3or4}/.gitignore (100%) rename {3 => 3or4}/3.org (100%) create mode 100644 3or4/4.org rename {3 => 3or4}/Chi.cf (100%) rename {3 => 3or4}/Chi.hs (100%) rename {3 => 3or4}/cabal.project (100%) rename {3 => 3or4}/chi.cabal (96%) rename {3 => 3or4}/flake.lock (100%) rename {3 => 3or4}/flake.nix (100%) rename {3 => 3or4}/interpreter/Main.hs (100%) create mode 100644 3or4/interpreter/Self.hs diff --git a/3/.envrc b/3or4/.envrc similarity index 100% rename from 3/.envrc rename to 3or4/.envrc diff --git a/3/.gitignore b/3or4/.gitignore similarity index 100% rename from 3/.gitignore rename to 3or4/.gitignore diff --git a/3/3.org b/3or4/3.org similarity index 100% rename from 3/3.org rename to 3or4/3.org diff --git a/3or4/4.org b/3or4/4.org new file mode 100644 index 0000000..08ebfa2 --- /dev/null +++ b/3or4/4.org @@ -0,0 +1,52 @@ +#+title: Assignment 4 +#+options: toc:nil +#+latex_header: \usepackage{parskip} + +In order to pass this assignment you have to get at least three points. + +Please provide your source code in a form which is easy to test, not, say, a PDF file. + +* (1p) +When is a function $f \in \mathbb{N} \rightarrow \mathbb{N}$ $\chi$ computable? + +** Answer +Whenever there is a closed expression $e$ such that $\forall n \in \mathbb{N}.\ e\ \ulcorner n \urcorner \Downarrow \ulcorner f\ n \urcorner$. +Further, $f$ is $\chi$ computable if one can reduce it to another function $g$ that is $\chi$ computable. + +* (2p) +Prove that the following functions is not $\chi$ computable (where /Exp/ is the abstract syntax of $\chi$): +\[ f \in \{ p \in Exp |\ p\ \text{is closed} \} \rightarrow \mathbb{B} \] +\[ f\ p = \text{if}\ p\ \text{terminates with the value}\ Zero()\ \text{then}\ true\ \text{else}\ false \] + +You should prove this by reducing the "intensional" halting problem (see the [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/lectures/L4.pdf][lecture slides]]) to this function. + +** Answer + +* (2p) +Implement $\chi$ substitution as a $\chi$ program. You should construct a $\chi$ expressions, let us call it /subst/, that given the representation of a variable $x$, a closed expression $e$, and an expression $e'$, produces the representation of the expression obtained by substituting $e$ for every free occurrence of $x$ in $e'$: +\[ 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. + +* (2p) +Implement a $\chi$ self-interpreter. You should construct a $\chi$ expression, let us call it /eval/, that satisfies the following properties: +- For any closed expressions $e$ and $v$, if $e \Downarrow v$ then $\text{eval}\ \ulcorner e \urcorner \Downarrow \ulcorner v \urcorner$. +- For any closed expressions $e$ and $v$, if $\text{eval}\ \ulcorner e \urcorner \Downarrow v$, then there should be some $v'$ such that $e \Downarrow v'$ and $v = \ulcorner v' \urcorner$. + +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: + + $\text{C}()\ \text{C}()$ + + $\text{case}\ \lambda x.x\ \text{of}\ {}$ + + $\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{C}(x) \rightarrow x }$ + + $\text{case} \text{C}()\ \text{of}\ { \text{D}() \rightarrow \text{D}() }$ + + $(\lambda x.\lambda y.x) (\text{rec}\ x = x)$ + +- 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 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 case (\lambda x.x) C() 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$. + +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. diff --git a/3/Chi.cf b/3or4/Chi.cf similarity index 100% rename from 3/Chi.cf rename to 3or4/Chi.cf diff --git a/3/Chi.hs b/3or4/Chi.hs similarity index 100% rename from 3/Chi.hs rename to 3or4/Chi.hs diff --git a/3/cabal.project b/3or4/cabal.project similarity index 100% rename from 3/cabal.project rename to 3or4/cabal.project diff --git a/3/chi.cabal b/3or4/chi.cabal similarity index 96% rename from 3/chi.cabal rename to 3or4/chi.cabal index e249920..6de4f5e 100644 --- a/3/chi.cabal +++ b/3or4/chi.cabal @@ -31,6 +31,7 @@ executable interpreter main-is: Main.hs hs-source-dirs: interpreter + other-modules: Self build-depends: base , chi , mtl diff --git a/3/flake.lock b/3or4/flake.lock similarity index 100% rename from 3/flake.lock rename to 3or4/flake.lock diff --git a/3/flake.nix b/3or4/flake.nix similarity index 100% rename from 3/flake.nix rename to 3or4/flake.nix diff --git a/3/interpreter/Main.hs b/3or4/interpreter/Main.hs similarity index 100% rename from 3/interpreter/Main.hs rename to 3or4/interpreter/Main.hs diff --git a/3or4/interpreter/Self.hs b/3or4/interpreter/Self.hs new file mode 100644 index 0000000..127f209 --- /dev/null +++ b/3or4/interpreter/Self.hs @@ -0,0 +1,8 @@ +-- | + +module Self where + +import Chi + +substExp :: Exp +substExp = parse ""