最近の検索
検索オプション
Division by zero in type theory: a FAQ 日本語訳
https://zenn.dev/leanja/articles/division_by_zero
たとえば C の未定義動作について、コンパイルエラーにする代わりにランダムな値を返すように追加の保証を与えた処理系みたいなイメージか。
未定義動作がどうなろうが「結局は踏まないパス」なのでどうでもいいし、定理証明なのだから最終的に踏まないパスであることは保証できると。
ZennDivision by zero in type theory: a FAQ 日本語訳
「内部的な個々の関数は状況次第で未定義動作を引き起こす可能性があるが、それらを呼ぶ側が正しく統制されているから結果的に未定義動作は起こさない」みたいなことをやっている印象。