pingu/Computeability
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Mab

Browse Source
This commit is contained in:
pingu
2025-12-02 15:16:01 +01:00
parent 69271905d1
commit b82602c614
1 changed files with 5 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
3or4/4.org
View File

@ -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. 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 ** 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) * (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'$: 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'$: