コラッツ予想がとけた ..
330:132人目の素数さん
18/06/29 03:51:44.66 iREabCnd.net
>>329
> Coqというプログラミング言語(定理証明支援系)では、再帰関数を作る際に、停止性をチェックされて、それをパスした関数だけが定義されます。
最近のCoqの現状は全く知らないのですが、そもそもCoqの文法に従って(チェックされなければ)停止しない関数を書けるような構文になってましたっけ?
Coqは構成的型理論と呼ばれるものに属する形式的体系の1つに基づいているので、その基づいている型理論に即して素直に項の構文(関数はこの構文を使って定義することになるので
この構文がその構成的型理論の体系が与えるプログラミング言語に相当する)を作ると、そもそも停止するか否かがわからないような関数を定義することは構文的に不可能だと理解しているのですが
それとも最近のCoqは書きやすさとかのためにgeneral recursionのような書き方を許す構文も導入しているのかなあ
次ページ続きを表示1を表示最新レス表示スレッドの検索類似スレ一覧話題のニュースおまかせリスト▼オプションを表示暇つぶし2ch
1839日前に更新/342 KB
担当:undef