Prolog でわかる TAPL 1日目 - TAPLの構成

太陽神ヘーリオス

ヘーリオス（古希: Ἥλιος , Hēlios）は、ギリシア神話の太陽神である。その名はギリシア語で「太陽」を意味する一般名詞と同一である。象徴となる聖鳥は雄鶏。

太陽は天空を翔けるヘーリオス神の4頭立て馬車であると古代ギリシア人は信じていた。

Wikipedia ヘーリオス より

TAPL は一階述語論理を用いています。一階述語論理は処理順を規定していないので規則を自由に選択肢して推論することができます。しかしそれでは自動的に実行できません。自動実行する一階述語論理のシステムがあれば自動実行することが可能なはず。一階述語論理を深さ優先探索 DFS で自動計算するシステムがあれば、、、。そう、その推論システムが Prolog です。

目次

• 1日目 - TAPLの構成☉
• 2日目 - 一階述語論理とProlog、MBNF☽
• 3日目 - 第Ⅰ部 型無しの計算体系 (1)♂
  • arith 型無し算術式 bool+nat(３,4章)
• 4日目 - 第Ⅰ部 形無しの計算体系 (2)☿
  • untyped 型無しラムダ計算 λ (7章)
  • fulluntyped フル型無しラムダ計算 bool+nat+float+λ+let+record(5,6章)
• 5日目 - 第Ⅱ部 単純型 (1)♃
  • tyarith 単純型付算術演算 bool+nat+単純型(8章)
  • simplebool 単純型付ラムダ計算+bool bool+nat+λ+単純型(10章)
  • fullsimple フル単純型付ラムダ計算 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+単純型(9,11章)
• 6日目 - 第Ⅱ部 単純型 (2)♀
  • fullref フル単純型付ラムダ計算+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+ref+top+bot+source+sink+単純型(13,18章)
  • fullerror フル単純型付ラムダ計算+エラー bool+λ+top+bot+try error+単純型(14章)
• 7日目 - 第Ⅲ部 部分型付け♄
  • rcdsubbot 単純部分型付ラムダ計算レコードbot λ+top+bot+record+単純部分型 (15,16章)
  • fullsub フル単純部分型付きラムダ計算 botなし bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+単純部分型 (15章)
  • bot 単純部分型付きラムダ計算+bot λ+top+bot+単純部分型(16章)
  • joinsub (16章) 実装なし？
  • joinexercise
• 8日目 - 第Ⅳ部 再帰型☉
  • fullisorec フル再帰型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+rec+fold+unfold+単純再帰型(20章)
  • fullequirec フル再帰型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+rec+単純再帰型(20章)
  • equirec 再帰型 λ+rec+単純再帰型(21章)
• 9日目 - 第Ⅴ部 多相性 (1)☽
  • reconbase 型再構築のベース bool+nat+λ+単純型(22章)
  • recon 型再構築 bool+nat+λ+型推論(22章)
  • fullrecon フル型再構築 bool+nat+λ+let+型推論(22章)
• 10日目 - 第Ⅴ部 多相性 (2)♂
  • fullpoly フル全称型、存在型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+all+some(23,24章)
• 11日目 - 第Ⅴ部 多相性 (3)☿
  • fullfsub フルF<: 有界量化 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+<:+all+some(26,28章)
  • fullfsubref フルF<: 有界量化+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+try error+ref+top+bot+<:+source+sink+all (27章)
  • purefsub 有界量化 λ+top+<:(28章)
• 12日目 - 第Ⅵ部 高階の型システム (1)♃
  • fomega +kind
  • fullomega フル型演算とカインド、高階多相 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+ref+all+some+kind(29,30章)
• 13日目 - 第Ⅵ部 高階の型システム (2)♀
  • fullfomsub フル有界量化サブ bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+<:+all+some+kind(26,31章)
  • fomsub 高階部分型付け λ+top+<:+all+kind(31章)
  • fullfomsubref フル有界量化サブ+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+try error+ref+top+bot+<:+source+sink+all+some+kind+import
• 14日目 - 第Ⅵ部 高階の型システム (3)♄
  • fullupdate フル純粋関数的オブジェクト 書き換え可能レコード bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+top+<:+all+some+kind+variance(32章)

はじめに

今年の Prolog カレンダーでは 2週間に渡って TAPL 用のソースコードを元に Prolog に移植したものを駆け足で紹介します。
Prolog に不慣れな方は多いと思いますが TAPL の理解には一階述語論理の理解が不可欠です。たかが、Prolog されど Prolog 。どのようなプラグラミング言語も最初は慣れないものなので辛いことを多くのプログラマは知っています。しかしながら、一度のその世界の素晴らしさを理解すれば全能感のようなものが得られることもご存知のはずです。Prologの世界、一階述語論理の世界を理解してしまえば、型システムの多くの知識にアクセスすることが可能になります。

Prolog は得意だが、静的型システムはちょっと、、、という方もいるでしょう。しかしながら、昨今 TypeScript や Ruby などに見られる漸進的型システムは将来開発が予想される漸進型システムの Prolog 版の登場のために必要な基礎知識がここに紹介されています。関数型言語と論理型言語には深い関わりあいがあり、双方に利点と欠点があります。お互いの相互理解がお互いの世界をより発展させるものと私は信じています。Prolog は死んだ? とんでもない。 Prolog は型理論の中のアルゴリズミックな規則の中に脈々と生き続けているのです。

TAPL では様々な演習や証明に多くのページが割かれています。しかしながら、まずは図に注目し実装をするだけでもボリュームがあります。したがってここでは実装と図に絞って概要します。

説明はかなりいい加減かもしれません。毎年アップデートする気持ちで取り組んでいきたいと思いますのでよろしくお願いします。

TAPL の構成

TAPL は以下のように６部に分けて構成されています:

• 第Ⅰ部 型無しの計算体系 (3,4日目)
• 第Ⅱ部 単純型 (5,6日目)
• 第Ⅲ部 部分型付け (7日目)
• 第Ⅳ部 再帰型 (8日目)
• 第Ⅴ部 多相性 (9,10,11日目)
• 第Ⅵ部 高階の型システム (12,13,14日目)

第Ⅰ部では静的型検査のない型無しの言語が説明されています。
第Ⅱ部では第Ⅰ部で作った言語用の単純な型システムが説明されています。
第Ⅲ部ではオブジェクト指向の継承関係にあるような親子関係を持つ部分型付けのある型システム、第Ⅳ部では型の中に同じ型を含むことが可能な再帰型のある型システムが書かれています。
第Ⅴ部ではオブジェクト指向のポリモーフィズムのような多相性、最後の第Ⅵ部では型システム上で計算可能な高階の型システムについて述べられています。

TAPL は主に Haskell や OCaml、SML のような関数型言語の型システムをまとめたものなのでオブジェクト指向言語に慣れている方は最初戸惑うかもしれません。しかし、実装を理解していくことで関数型言語の研究によって蓄積されてきた型システムの基礎的な知識を学ぶことができます。

第Ⅰ部 型無しの計算体系 (3,4日目)

• arith 型無し算術式 bool+nat(３,4章)
• fulluntyped フル型無しラムダ計算 bool+nat+float+λ+let+record(5,6章)
• untyped 型無しラムダ計算 λ (7章)

もう少し詳しく見ていきましょう。
型無しの計算体系では、主にBNFスタイルの表記を使って言語の構文を定義し、一階述語論理を用いて操作的意味論の変換規則を説明しています。
arith,fulluntyped,untypedの3つの言語があります。
arithは形無し算術式でboolとnatのある言語です。fulltypedは全機能 (bool+nat+float+λ+let+record) を突っ込んだ実装、untypedは形無しラムダ計算の本質のみを抜き出した実装です。

第Ⅱ部 単純型 (5,6日目)

• tyarith 単純型付算術演算 bool+nat+単純型(8章)
• fullsimple フル単純型付ラムダ計算 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+単純型(9,11章)
• simplebool 単純型付ラムダ計算+bool bool+nat+λ+単純型(10章)
• fullref フル単純型付ラムダ計算+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+ref+top+bot+source+sink+単純型(13,18章)
• fullerror フル単純型付ラムダ計算+エラー bool+λ+top+bot+try error+単純型(14章)

単純型の部は５つのコードが対応しています。継承のような部分型付けやポリモーフィズムのようなものがない単純な型システムを実装し、参照(書き換え可能な変数)のある拡張と、エラー処理が含まれた言語を作ります。
tyarithはarithに単純な型システムを追加したものです。
fullsimple は fulluntyped に単純型システムを追加したもの、 simplebool は untyped に単純型システムを加えたものです。
fullref はフル実装のラムダ計算に加えて書き換え可能な変数である参照を加えたものであり、fullerrorはフル実装のラムダ計算にエラー処理を加えたものです。

第Ⅲ部 部分型付け (7日目)

• rcdsubbot 単純部分型付ラムダ計算レコードbot λ+top+bot+record+単純部分型 (15,16章)
• fullsub フル単純部分型付きラムダ計算 botなし bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+単純部分型 (15章)
• bot 単純部分型付きラムダ計算+bot λ+top+bot+単純部分型(16章)
• joinsub (16章) 実装なし？
• joinexercise

部分型付けの部では、オブジェクト指向の親子関係を持ったちょっと複雑な型システムについて書かれています。
あれ？継承も何もないじゃないか、と思う方も多いかもしれません。
レコードはあるけど、オブジェクトはどこにもないじゃないか。

オブジェクトはレコードに関数が含まれた物です。レコードの部分型付けのことがわかれば、オブジェクトの継承についても理解が容易となります。

構造的な部分型付け関係を用いてJSONのオブジェクトのようなレコードの部分型を実装することで部分型付けを理解できれば、さまざまな部分型付け関係を理解できます。

Prolog の家系図を推論するようなことがこんなところで生かされているわけです。

第Ⅳ部 再帰型 (8日目)

• fullisorec フル再帰型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+rec+fold+unfold+単純再帰型(20章)
• fullequirec フル再帰型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+rec+単純再帰型(20章)
• equirec 再帰型 λ+rec+単純再帰型(21章)

自分の中に自分がある型。そのような型はこれまで説明してきた型システムでは実装できません。再帰関数を作るように再帰的な型があれば、自分の中に自分があるような型システムが実現できます。 第Ⅳ部 再帰型では２つの再帰型を表す形式について書かれています。Norminalな型システムなら簡単なんですが、構造的な型システムだと難しいから名前をつける。そんな感じでしょうか？

第Ⅴ部 多相性 (9,10,11日目)

• reconbase 型再構築のベース bool+nat+λ+単純型(22章)
• recon 型再構築 bool+nat+λ+型推論(22章)
• fullrecon フル型再構築 bool+nat+λ+let+型推論(22章)
• fullpoly フル全称型、存在型 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+all+some(23,24章)
• fullfsub フルF<: 有界量化 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+<:+all+some(26,28章)
• fullfsubref フルF<: 有界量化+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+try error+ref+top+bot+<:+source+sink+all (27章)
• purefsub 有界量化 λ+top+<:(28章)

さあ、いよいよ、我々は多相性の世界に入っていきます。
型の再構築はいわゆる型推論の機能について説明されています。型理論の世界では型再構築っていうんですね。
全称型、存在型、有界量化、、、。なんだか難しそうな用語がでてきましたが、その正体やいかに、、、。

第Ⅵ部 高階の型システム (12,13,14日目)

• fomega +kind
• fullomega フル型演算とカインド、高階多相 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+ref+all+some+kind(29,30章)
• fullfomsub フル有界量化サブ bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+<:+all+some+kind(26,31章)
• fomsub 高階部分型付け λ+top+<:+all+kind(31章)
• fullfomsubref フル有界量化サブ+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+try error+ref+top+bot+<:+source+sink+all+some+kind+import
• fullupdate フル純粋関数的オブジェクト 書き換え可能レコード bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+top+<:+all+some+kind+variance(32章)

最終の第Ⅵ部 高階の型システムでは、今まで積み上げてきた型システムに加え、更に上の階層にある型システムについて書かれています。

最終的に構築された書き換え可能なオブジェクトを持つ型システムと、イムータブルな関数的オブジェクトシステムに到達するまでのいくつかの型システムについてかかれています。

ラムダキューブとは何なのか？様々な謎?が解き明かされます。

まとめ

初日の今日は、TAPL の全体像を眺め概要を説明しました。

さらなる詳細な証明を行うためには定理証明支援システムである Coq、 Issabele、 Agda などを用いて証明することができます。Prolog でも定理証明支援システムは作ることができますが、素の Prolog にその能力はないので、ここではそこまで触れません。ソフトウェアの基礎などを読むことで証明の世界を実装しながらより深く理解することができるでしょう。

Prolog を用いると TAPL の図と同様の考え方で実装することができます。
Prolog は万能ではありません。しかしながら、図を見て実装し実験してみる分には Prolog が最適なのかもしれません。

Rooster
From Wikipedia, the free encyclopedia

For other uses, see Rooster (disambiguation).
"Cockadoodledoo" and "Cocka-doodle-doo" redirect here. For the nursery rhyme, see Cock a doodle doo.

A rooster, also known as a cockerel or cock, is a male gallinaceous bird, with cockerel being younger and rooster being an adult male chicken (Gallus gallus domesticus).