2023.06.08
https://gyazo.com/375434362bc69da2a7f1f6058c30e40c
メモ
思った
今日は眠い/腹が減らない/やる気のないの3重苦で大変だった
やった
たとえば原始再帰的関数として大真面目に書くと,↓の通りになると思うが,こんなの厳密にちゃんとやってられないだろうとはずっと思う. 加算$ \mathsf{add}(\mathtt{x}_0,\mathtt{x_1}) \equiv \mathsf{prec}_{\mathsf{proj}^2_0,\mathsf{comp}_{\mathsf{proj^3_2},\mathsf{s}}}(\mathtt{x}_0,\mathtt{x_1})
乗算$ \mathsf{mul}(\mathtt{x}_0,\mathtt{x}_1) \equiv \mathsf{prec}_\mathsf{zero^2,\mathsf{comp}_{\mathsf{proj}^3_0,\mathsf{proj}^3_2,\mathsf{add}}}(\mathtt{x}_0,\mathtt{x_1}) \equiv \mathsf{prec}_\mathsf{zero^2,\mathsf{comp}_{\mathsf{proj}^3_0,\mathsf{proj}^3_2,\mathsf{prec}_{\mathsf{proj}^2_0,\mathsf{comp}_{\mathsf{proj^3_2},\mathsf{s}}}}}(\mathtt{x}_0,\mathtt{x_1})
ある記号列$ \sigmaを受け取ったとき直ちに記号列$ \mathtt{s}\sigmaを返す装置を後者関数と呼ぶ.
読んだ