エントリーの編集
エントリーの編集は全ユーザーに共通の機能です。
必ずガイドラインを一読の上ご利用ください。
OCamlでlet recを使わずにfact関数を定義する - にわとり小屋でのプログラミング
記事へのコメント0件
- 注目コメント
- 新着コメント
このエントリーにコメントしてみましょう。
注目コメント算出アルゴリズムの一部にLINEヤフー株式会社の「建設的コメント順位付けモデルAPI」を使用しています
- バナー広告なし
- ミュート機能あり
- ダークモード搭載
関連記事
OCamlでlet recを使わずにfact関数を定義する - にわとり小屋でのプログラミング
今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数の... 今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうからだ。次のシンプルな例を見てみよう。 Inductive t (A: Set) : Set := | T : (t A -> A) -> t A. 一見なんの問題も無さそうな この型定義は失敗し、次のようなコンパイルエラーが出力される。 Error: Non strictly positive occurrence of "t" in "(t A -> A) -> t A".もしこの型が定義できたとすると次のような関数が定義できてしまう。 Definition ワォ (T f) := f (T f). ここで (ワォ (T ワォ)