diff --git a/3or4/4.org b/3or4/4.org index 87d74ee..f2b9d58 100644 --- a/3or4/4.org +++ b/3or4/4.org @@ -21,6 +21,11 @@ Prove that the following functions is not $\chi$ computable (where /Exp/ is the 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 +The halting problem can be reduced to this problem, by the expression: +\[ \lambda p. f\ ((\lambda \_. Zero()) p) \] + +In the case where p terminates, the $(\lambda \_. Zero()) p$ would evaluate to $Zero()$, and therefore $f ((\lambda \_. Zero()) p)$ would evaluate to true. +In the case where p does not terminate, then $(\lambda \_. Zero()) p$ would not evaluate to $Zero()$ as $p$ would not terminate with a value, therefore $f ((\lambda \_. Zero()) p)$ would evaluate to false. * (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'$: