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

Hand ins

Browse Source
This commit is contained in:
pingu
2025-12-09 15:43:08 +01:00
parent df5c80b5df
commit c7928ec703
2 changed files with 9 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
5.org
View File

@ -28,7 +28,7 @@ Which means
&= \llbracket \underline{\text{has-fixpoint}}\ \ulcorner \lambda n. ((\lambda \_. n)\ p) \urcorner \rrbracket \\
&= \ulcorner \text{has-fixpoint}(\lambda n. ((\lambda \_. n)\ p)) \urcorner \\
&= \begin{cases}
\ulcorner \text{true} \urcorner &\quad \text{if}\ \exists v \in Exp. \llbracket p \rrbracket = v,\\
\ulcorner \text{true} \urcorner &\quad \text{if}\ \exists v \in Exp. \llbracket p \rrbracket = v\ \text{(due to strictness in application)},\\
\ulcorner \text{false} \urcorner &\quad otherwise
\end{cases}
\end{align*}
@ -138,7 +138,8 @@ Let a two-tape Turing machine be defined by the following:
\UnaryInfC{$\text{\textvisiblespace} \notin \Sigma$}
\AxiomC{$\Gamma$ is a finite set}
\UnaryInfC{$\Sigma \cup \{\text{\textvisiblespace}\} \subseteq \Gamma$}
\AxiomC{$\delta \in S \times \Gamma \times \Gamma \rightharpoonup S \times (\Gamma \times \{L,R\}) \times (\Gamma \times \{L,R\})$}
\AxiomC{$\delta \in S \times \Gamma \times \Gamma \rightharpoonup$}
\UnaryInfC{$S \times (\Gamma \times \{L,R\}) \times (\Gamma \times \{L,R\})$}
\alwaysSingleLine
\QuaternaryInfC{$(S,s_0, \Sigma, \Gamma, \delta) \in \text{TM2}$}
\end{prooftree}