日々の流転

λ. 計算と論理のための自然枠組NF/CAL by 佐藤 雅彦

本論文では，計算機上での証明記述および検証を支援するシステムNF/CALを紹介する．NF/CALの設計はフレーゲによる判断の分析の影響を受けており，人間が自然言語を用いて日常的に行う判断活動を自然に形式化したものになっている．

ずっと積読中だったものを消化。ワークショップの“Types for Verification”で“A simple theory of expressions”という講演を聴いたときには何が嬉しいのかよく分からなかったが、以下に引用する部分を読んでようやく動機が理解できた。

これらのシステムの多くは型理論に基づいており，もっぱら専門家による使用を前提としている．そのためシステムの利用には型理論の知識が必要となり，学部で計算や論理を教育するためのシステムとしては不適当である．本稿で紹介した式の理論は，計算や論理の基礎的事項を，最初から説明するための必要性から考案したものであるが，同時に我々が日常的に用いる自然言語が本来持っている構造を自然に反映したものになっている．

しかし、NF/CAL面白そうだな。 CALは昔使わせてもらったことがあって、そのときには挫折してしまったのだけど、出来たらまた試してみたいものだ。