名残

プレゼント・デイ　プレゼント・タイム

操作的意味論とか数理論理学とか Coq とか

TL;DR

  • いろんな本を使って操作的意味論と数理論理学を学び始めた
  • MBP にインスコした CoqIde で Coq を書き始めた
  • #100DaysOfCS を始めた

はじめに

先日、大学の図書館でいろいろと本を借りてきました。

操作的意味論や数理論理学を学んで、プログラミング言語についての理解を深めることが目的です。
今回は上で太文字にしてある２冊を扱いますが、他の本についても、また別の記事で言及したいと思います。

操作的意味論について

CoPL を使って学んでいます。操作的意味論は、プログラムをどのように操作・計算して実行結果を得るか、という視点からの「意味の与え方の体系」です。プログラムの意味論はこれを含めて３種類あり、あとの２つは「公理的意味論」と「表示的意味論」です。「プログラム意味論」という本で詳しく解説されているらしいので、後々学んでいきたいと思います。

CoPL には優れた「演習システム」があり、Webサイト上で演習問題を解いて、自動採点機能を利用することができます。今は算術式の評価・簡約に関する演習問題を解き進めています。今後メタ定理の証明を行うので、後述する Coq で記述してみようかなぁと思ってます。

数理論理学について

「情報科学における論理」という本を使っています。
今は第１章「命題論理」で充足可能性について学んでいます。

CoPL で今後学ぶ「推論」などの分野で、この数理論理学で学んだことが役に立つらしいです。

Coq に入門した

ここまで紹介してきた２冊には、証明問題がいくつも掲載されています。
もちろん僕も手を動かしてそれを解いてますが、PC上で専用の言語を使って半ば機械的に証明をしたり、証明の過程をテキストに起こして GitHub 等で管理したいという思いがありました。

このような理由から、前々から気になっていた Coq に触れてみることにしました。
Coq はプログラムの仕様を検証するためによく用いられる証明支援システムです。
今の僕にはよく分かりませんが、高階述語論理というものを採用しているため、検証器としての表現力はかなり高いらしいです。

環境構築

MacBook Pro (2017) に導入することを想定しています。
まず、GitHub リポジトリの Releases ページから dmg ファイルを落とします。
今回は Pre-release ではなく Latest release の 8.8.2 をダウンロードしました。
マウントすると .app ファイルが入っているので、Applications フォルダに移動して起動します。

さっそく定理証明してみる

手始めに、f(x) = x + 100, g(x) = x - 100 を定義して、定理 g(f(x)) = x が成り立つことを証明します。 エンジニアHubというサイトのこの記事を参考にしました。見よう見まねで証明を記述してみます。

帰納法を使って証明してみる

こんな風に、induction タクティクスで帰納法を使うことができます。
フォロワーさん曰く、fix タクティクスや inversion タクティクスを用いることも出来るらしいです。

※ タクティクス：Coq の証明開発モードで用いる道具

まとめ・目標

初のブログ記事ですが、いかかでしたか？

実は昨日から、100DaysOfCS (CS=Computer Science) ということで、100日間CS関連の理論を学んで、毎日進捗を報告し続けるチャレンジを始めています。

ある程度進捗が出たら、まとめてこのようなブログ記事にして公開するので、これからもよろしくお願いします！