  |
はてなキーワード: ラムダ計算とは
コーンフレークじゃなくて、Haskellだとして、全体のネタを書き直してくださいっていう指示した結果
ボケ＆ツッコミ「お願いしますー ありがとうございますー」
ツッコミ「あー ありがとうございますー ねっ 今Githubでスターをいただきましたけどもね」
ボケ＆ツッコミ「ありがとうございますー」
ツッコミ「ねー 有り難いですよ ほんとにね」
ボケ「入れておきましょう」
ボケ「いきなりですけどね うちのオカンがね 好きなプログラミング言語があるらしいんやけど」
ツッコミ「プログラミング言語の名前忘れてもうて どうなってんねそれ」
ツッコミ「分からへんの？ いや ほな俺がね おかんの好きなプログラミング言語 ちょっと一緒に考えてあげるから どんな特徴ゆうてたかってのを教えてみてよ」
ボケ「あのー関数型言語で、型システムが強力で、遅延評価するやつやって言うねんな」
ツッコミ「おー Haskellやないかい その特徴はもう完全にHaskellやがな」
ツッコミ「すぐ分かったやん こんなんもー」
ツッコミ「いやそうやろ？」
ボケ「オカンが言うには 将来の夢はそれで書かれたOSを使うことやって言うねんな」
ツッコミ「あー ほなHaskellと違うかぁ Haskell製のOSなんてまだ無いもんね」
ボケ「そやねん」
ツッコミ「HaskellはOSを作るのには向いてへんからなぁ」
ボケ「そやねんな」
ツッコミ「な？ Haskell側もOS開発に任命されたら荷が重いよあれ」
ボケ「そやねんそやねん」
ツッコミ「Haskellってそういうもんやから ほなHaskellちゃうがなこれ」
ボケ「そやねん」
ツッコミ「あれほなもう一度詳しく教えてくれる？」
ツッコミ「Haskellやないかい モナドは確かに難しいねんHaskellの でも俺はね あれはHaskellの良いところやと思うねん 俺の目は騙されへんよ 俺騙したら大したもんや」
ボケ「まあねー」
ツッコミ「ほんであれよー いざ使ってみたらね モナドのおかげでコードがスッキリするねん 俺は何でもお見通しやねんから Haskellのモナドなんて」
ツッコミ「そうやろ」
ボケ「オカンが言うには プロダクションで使うにはまだ早いって言うねんな」
ツッコミ「ほなHaskellちゃうやないかい プロダクションでHaskell使ったら 上司がひっくり返すもんね Haskellはねー まだ研究段階やから実務では使いにくいねん」
ボケ「そやねんそやねん」
ツッコミ「な？ Haskell使ってみたらだんだん罠が見えてくるから 最後ちょっとだけ避けてまうねんあれ」
ボケ「そやねんそやねん」
ボケ「そやねんな」
ツッコミ「Haskellちゃうがな ほな もうちょっとなんか言ってなかった？」
ボケ「学生の頃 なんでみんな憧れるんか分からんかったらしいねん」
ツッコミ「Haskellやないかい 学生の頃はHaskellとOCamlとLispに憧れるんやから あとSmalltalkも憧れたな Haskellそんなもんよ」
ツッコミ「そうやろ」
ボケ「オカンが言うには 関数型プログラミングの教科書に必ず載ってるっていうねん」
ツッコミ「ほなHaskellやないかい 教科書のサンプルコードにHaskellのコードが出てこんわけないやん」
ツッコミ「Haskellはね 関数型プログラミングの王道中の王道やねん」
ツッコミ「Haskellや絶対 ほな ほなもうちょっとなんかゆうてなかったか？」
ツッコミ「Haskellやないかい Yesodとかあるやろ な？ RubyとかPythonの次はHaskellが来るって言われてるねん 俺はそう思うよマジで Haskellや絶対」
ツッコミ「そうやて」
ボケ「オカンが言うには ジャンルでいうたら数学やっていうねん」
ツッコミ「ほなHaskellやないかい ジャンルで数学言うたらHaskellしかあらへんやん な？ Haskellは数学の理論がベースになってるんやで ラムダ計算とか圏論とかな」
ボケ「そやねんそやねん」
ツッコミ「ほなHaskellに決まりやないかい ほなもうちょっとなんかゆうてなかった？」
ツッコミ「Haskellやないかい Haskellは変数が不変やから 変数に感謝するのは当然やねん ね？ 状態変更せんと安心して使えるからな」
ボケ「そやねんそやねん」
ツッコミ「Javaとかの変数は裏切るからアカンねん Haskellの変数は一生そばにおってくれるから最高やで」
ボケ「でも分かれへんねん」
ツッコミ「分からへんことない おかんの好きなプログラミング言語はHaskell もぉ」
ボケ「でもオカンが言うには Haskellではないって言うねん」
ツッコミ「ほなHaskellちゃうやないかい オカンがHaskellではないと言うんやから Haskellちゃうがな」
ボケ「そやねん」
ツッコミ「先ゆえよ 俺がラムダ計算の説明してる時どう思っててんお前」
ツッコミ「ホンマに分からへんがなこれ どうなってんねんもう」
ボケ「んでオトンが言うにはな」
ツッコミ「オトン？」
・もっと根源的な問題として、推論規則の「一覧表」があるとして、あるマスの記号列とあるマスの記号列の関係それ自体を厳密に記述することは可能なのか？と思う。
はい. もちろんできます. 例えば数理論理学の本などを参照していただければ, 証明体系などの数学的定義が与えれらています.
私は「書き換え」のように自然言語を使って表現していますが, これらの操作などももちろん数学的に定義されます. 「操作」とは何かという疑問をお持ちでしたらラムダ計算の理論が参考になると思います. そしてこれらの操作は全て計算可能です, 平たくいうとプログラムとして実装できます. これらは全く感覚的なものではありません.
・（その他の部分に関して)
何が問題意識としてあるのかが私ははっきりとつかめていません. すいません.
例えば自然数の概念を共有していれば上記の概念(証明体系等)は一意的に共有できるものです. 一方で例えば何も共有していない全く無の人にこれらの概念を共有するのは困難だと思われます.
卑近な例でしたら, 数学を全く知らない人に突然これらの定義を見せたら, ただの絵や呪文に見えるでしょう. (私はそれはそうだと思います. 数学に対してどういう普遍性を求めているのか分かりませんが. )
最後に, 哲学的にそのようなトピックを議論したいのであれば, 無理に数学の言葉を使わなくとも可能だと思われます. 時には数学における言葉遣いが通常の言葉遣いと異なる場合もあります. また度々言及されいる事柄のいくつかは様々なな分野で歴史的に議論, 研究されているトピックがいくつもあります. いくつかの文献を読んでみて一度整理されると, 誤解, 車輪の再発明を避けることになりますし, あなたがどういう問題, 問題意識を持っているかをきちんと言語化する助けになると思います. それに加えて, これまで人々が様々な学問領域で積み重ねてきた多くの結果に敬意を払うことが重要であると私は考えます.
の具体的になんて本(ネットのpdfでもよい)の何ぺージあたりからが元増田の問いにとって核心なのって話よね
てか、ラムダ計算よりむしろ記号論理学のほうが学問としての領域が気持ち広くなってね？
2. ラムダ項M, Nに対して (M N) はラムダ項。この形のラムダ項を適用（ラムダ適用）という。
(後略)
という定義があるんだけど、これに基づけば(x x)というのもラムダ項じゃないのって思ってた。
でもラムダ式で(x x)なんて形のは見たことないし、違うんだろうなと。
でも論理的にはなぜ違うのか全く納得できてないので(納得感が正しさにとって問題じゃないとはいえあえて言うが)(x x)だってラムダ式でしょって胸を張って言い張れる。
コンピューターサイエンス自体がふんわりしていて、範囲が広すぎるから分からんでもない。
(ある程度アルゴリズムとデータ構造は既知のものとして)、計算理論や離散数学辺りを浅くてもいいから、さらっておくといいよ。
よさげなのを探してみた。
https://www.youtube.com/@hayamizu
「計算の仕組み 〜オートマトンからラムダ計算まで〜」 関山 太朗 - 国立情報学研究所 2020年度 市民講座 第3回 - YouTube
https://www.youtube.com/watch?v=DaiUQvE8O1U
Yoshio Okamoto - YouTube
https://www.youtube.com/@okamoto7yoshio
情報系の数学 第０回：どうして情報系で数学を学ぶのか？ - YouTube
何かの参考とかにしたらダメです。書き始めて半年経つんだけどこっからどう直したらいいんだか（何をゴールにしたらいいのか）わからない。。
追記：合流性とか強正規化可能性とか停止性とか、全部チューリング不完全で、事前の静的解析で使うメモリの最大量が確定できる、とかそういう風に読み替えられる人を増やしたいのです、数式の添え字とΣと∫にびびらない人を増やしたいようなもので
数理論理学の一分野である証明論から成長した、数理論理学と理論計算機科学の境界領域の研究領域である型理論(type theory)は、大規模なプログラムの内的な整合性のチェックを行うための方法論を必要とする情報処理技術の分野で関心を集めている。
そもそも「型」(type)とは何か。プログラミング言語は一般的にはレコードや関数といったプログラムを構成する「値」(value)の定義をする道具である(*1)。その言語のコンパイラ作成者はこれらレコードや関数などの値、もしくは第一級の対象(first-class object)の種類を区別する型システム(type system)を必要とする。抽象代数学の観点からすると、「型」とはこれらの値もしくは第一級の対象が属する高階の対象(higher order object)としての空間(space)ないし代数系(algebraic system)で、型システムはそれら「型」とそれら相互の関係(relation)つまり型のなす順序構造(order structure)ないし束構造(lattice structrure)であるといえる。
プログラムを構成する値すべてに型が付くためには、曖昧でない(*2)こと、自己矛盾していないこと、悪循環を含まないこと、それぞれの値の内容をチェックするために無限の時間を要しない(*3)ことなどが必要で、これらを満たすなら、プログラムは有限時間で実行を終え、停止する。手続き型言語では無限ループ、型無しラムダ計算では無限再帰によって型付け不能なプログラムを書くことができるが、型理論はこれらのチューリング完全な計算機を意図しない停止しないプログラムから守る装甲でもあり、再帰やメモリ確保で好き勝手をさせないための拘束具でもある。型が付くプログラムには単に停止するというだけでなく、可能な実行経路（訂正：経路→方法）のすべてで同じ結果を出すなど種々の良い性質がある。
1)この定義は現実に使われているプログラミング言語の特徴を覆い切れていない、狭い不満足な定義だが本稿では都合上この定義に立脚して限定的に議論する。例えば変数(variable)というものを持つプログラミング言語もあり広く使われているが、これについてはレコードや関数と同じように性質の良いものとして扱うことが難しい。難しさの原因は次の注の内容と関連する。近年は変数を扱うかわりに値の不変のコピー(immutable copy)やその参照に名前を付ける機能を持つプログラミング言語が増えている。
2) 現実の情報システムでは、COBOL言語のレコード再定義やC言語の共用体、一般的な関数ポインタやVisual Basic言語のvariant型変数のように、同一領域に異なる型の値が共存する共用型(union type)の値がしばしば必要となる。共用型の値はgoto文を排除した構造化／オブジェクト指向プログラミングにおいて条件キャストやクラス分岐などによる実行経路の複雑さの主要な原因になるが、これは和型(sum type)すなわち相異なる型の非交和(disjoint sum)として定義することで曖昧さなく定義できる。
3) ゲームプログラムやネットワークサービスにおいてしばしばみられるように、入力として無限リストや任意に深い木のようなものを想定する場合には明らかに（条件を満たさない限り）停止しないことが正しい動作となり、この場合は最外周のループを（←どうする？）メモリリークを起こさないなど別の考慮が必要となる。
うぜえ。
計算可能性の理論やラムダ計算がLispを産んだように、プログラム意味論や圏論はHaskellを産んだ。
プログラム意味論では変数の型が議論の最小単位で、関数やプログラムはある型の変数を別の型の変数へ変換する変換器として記述される。
だから本質的に、型が無いとプログラムという概念が存在できないことになる。
で、このアカデミックな議論が普段書くコードにどう影響を与えるかというと、実はほとんど影響がない。
もちろん知っていた方がよりエレガントなコードを書けるだろうが、必須ではない。
圏論を知っている必要があるのは、Haskellを設計する人達だけだ。
#毛の壁 氏について。
人格的なことは触れないとしても、みんな思うのは、「どうして色々読んでるっぽいのにああなれるのか」ということだと思うので、ちょっと考察してみた。
恐らく氏は、センテンス、辞書の項目くらいの長さのものの把握には長けている。ただ、文脈を読むとか、全体像を把握するとかそういう能力が欠如してる。多分、話の筋に展開があるとセクション単位のものも把握できない。
そのため、ミクロの理解のみで全体を捉えようとするから、認識と現実に齟齬が起きる。また、一見同じ形をしているが、論じるべき階層がそもそも異なるようなことを混同してしまう。もちろん物事の体系的な理解も出来ない。そうなると多分いわゆる構造化が必要なレベルのソースも書けない。形式的な定義や証明の理解も怪しいのだろう。
そう考えると、関数型プログラミングが遅延評価だと思うのも、評価戦略としての遅延とライブラリレベルで提供される lazy/force を混同するのも、S式と Lisp 構文を混同するのも理解できる。アカデミックな体系的学習が必要な haskell, ML に手が伸びないのもわかるし、数学的基礎と言っておきながら基礎論が全く出てこないのも分かる。ラムダ計算を知らないとすると、Lisp のあのへんてこな改造(?)もうなずける。局所的なスコープとクラス／モジュール単位のアクセス制限の話で揉めてたのは、多分モジュールやクラスをまともに扱ったことがないからなのだろう。それは github の珍妙なコードからもなんとなく推測できる。
第1章 並行プログラミングとGHC (上田和紀) 1.1 はじめに 1.2 ターゲットを明確にしよう 1.3 はじめが大切 1.4 GHCが与える並行計算の枠組み 1.4.1 GHCにおける計算とは，外界との情報のやりとり(通信)である 1.4.2 計算を行う主体は，互いに，および外界と通信し合うプロセスの集まりである 1.4.3 プロセスは，停止するとは限らない 1.4.4 プロセスは，開いた系(open system)をモデル化する 1.4.5 情報とは変数と値との結付き(結合)のことである 1.4.6 プロセスは，結合の観測と生成を行う 1.4.7 プロセスは，書換え規則を用いて定義する 1.4.8 通信は，プロセス間の共有変数を用いて行う 1.4.9 外貨も，プロセスとしてモデル化される 1.4.10 通信は，非同期的である 1.4.11 プロセスのふるまいは，非決定的でありうる 1.5 もう少し具体的なパラダイム 1.5.1 ストリームと双方向通信 1.5.2 履歴のあるオブジェクトの表現 1.5.3 データ駆動計算と要求駆動計算 1.5.4 モジュラリティと差分プログラミング 1.5.5 プロセスによるデータ表現 1.6 歴史的背景と文献案内 1.7 並行プログラミングと効率 1.8 まとめ 第2章 様相論理とテンポラル・プログラミング (桜川貴司) 2.1 はじめに 2.2 様相論理 2.3 時制論理 2.4 多世界モデル 2.5 到達可能性と局所性 2.6 純論理プログラミングへ向けて 2.7 Temporal Prolog 2.8 RACCO 2.9 実現 2.10 まとめと参考文献案内 第3章 レコード・プログラミング (横田一正) 3.1 はじめに 3.2 レコードと述語の表現 3.3 レコード構造とφ-項 3.3.1 φ-項の定義 3.3.2 型の半順序と束 3.3.3 KBLとLOGIN 3.4 応用――データベースの視点から 3.4.1 演繹データベース 3.4.2 レコード・プログラミングとデータベース 3.4.3 いくつかの例 3.5 まとめ 3.6 文献案内 第4章 抽象データ型とOBJ2 (二木厚吉・中川 中) 4.1 はじめに 4.2 抽象データ型と代数型言語 4.2.1 抽象データ型 4.2.2 代数型言語 4.2.3 始代数 4.2.4 項代数 4.2.5 項書換えシステム 4.3 OBJ2 4.3.1 OBJ2の基本構造 4.3.2 モジュールの参照方法 4.3.3 混置関数記号 4.3.4 モジュールのパラメータ化 4.3.5 パラメータ化機構による高階関数の記述 4.3.6 順序ソート 4.3.7 属性つきパターンマッチング 4.3.8 評価戦略の指定 4.3.9 モジュール表現 4.4 おわりに 第5章 プログラム代数とFP (富樫 敦) 5.1 はじめに 5.2 プログラミング・システム FP 5.2.1 オブジェクト 5.2.2 基本関数 5.2.3 プログラム構成子 5.2.4 関数定義 5.2.5 FPのプログラミング・スタイル 5.3 プログラム代数 5.3.1 プログラム代数則 5.3.2 代数則の証明 5.3.3 代数則とプログラム 5.4 ラムダ計算の拡張 5.4.1 ラムダ式の拡張 5.4.2 拡張されたラムダ計算の簡約規則 5.4.3 そのほかのリスト操作用演算子 5.4.4 相互再帰的定義式 5.4.5 ストリーム(無限リスト)処理 5.5 FPプログラムの翻訳 5.5.1 オブジェクトの翻訳 5.5.2 基本関数の翻訳 5.5.3 プログラム構成子の翻訳 5.5.4 簡約規則を用いた代数則の検証 5.6 おわりに 第6章 カテゴリカル・プログラミング (横内寛文) 6.1 はじめに 6.2 値からモルフィズムへ 6.3 カテゴリカル・コンビネータ 6.3.1 ラムダ計算の意味論 6.3.2 モルフィズムによる意味論 6.3.3 カテゴリカル・コンビネータ理論CCL 6.4 関数型プログラミングへの応用 6.4.1 関数型プログラミング言語ML/O 6.4.2 CCLの拡張 6.4.3 CCLに基づいた処理系 6.4.4 公理系に基づいた最適化 6.5 まとめ 第7章 最大公約数――普遍代数，多項式イデアル，自動証明におけるユークリッドの互除法 (外山芳人) 7.1 はじめに 7.2 完備化アルゴリズム 7.2.1 グラス置換えパズル 7.2.2 リダクションシステム 7.2.3 完備なシステム 7.2.4 完備化 7.2.5 パズルの答 7.3 普遍代数における完備化アルゴリズム 7.3.1 群論の語の問題 7.3.2 群の公理の完備化 7.3.3 Knuth-Bendix完備化アルゴリズム 7.4 多項式イデアル理論における完備化アルゴリズム 7.4.1 ユークリッドの互除法 7.4.2 多項式イデアル 7.4.3 Buchbergerアルゴリズム 7.5 一階述語論理における完備化アルゴリズム 7.5.1 レゾリューション法 7.5.2 Hsiangのアイデア 7.6 おわりに 第8章 構成的プログラミング (林 晋) 8.1 構成的プログラミング？ 8.2 型付きラムダ計算 8.3 論理としての型付きラムダ計算 8.4 構成的プログラミングとは 8.5 構成的プログラミングにおける再帰呼び出し 8.6 おわりに：構成的プログラミングに未来はあるか？ 第9章 メタプログラミングとリフレクション (田中二郎) 9.1 はじめに 9.2 計算システム 9.2.1 因果結合システム 9.2.2 メタシステム 9.2.3 リフレクティブシステム 9.3 3-Lisp 9.4 リフレクティブタワー 9.5 GHCにおけるリフレクション 9.5.1 並列論理型言語GHC 9.5.2 GHCの言語仕様 9.5.3 GHCのメタインタプリタ 9.5.4 リフレクティブ述語のインプリメント 9.6 まとめ
第1章 新しいプログラミング・パラダイムをめぐって (井田哲雄) 1.1 はじめに 1.2 プログラミング・パラダイムの形成 1.3 プログラミング・パラダイムの展開 1.4 パラダイムと作法と構造化プログラミング 1.5 構造化プログラミングを超えて 1.6 関数型プログラミング，論理型プログラミング，対象指向プログラミング 1.7 新しいプログラミング・パラダイム 1.8 まとめ 第2章 ラムダ計算と高階プログラミング (横内寛文) 2.1 はじめに 2.2 ラムダ計算 2.3 最左戦略 2.4 コンビネータによる計算 2.5 まとめ 第3章 マルセイユProlog，Prolog Ⅱ，Prolog Ⅲ 3.1 はじめに 3.2 準備 3.2.1 述語 3.2.2 項 3.2.3 項の単一化 3.2.4 節およびHorn節 3.2.5 論理式の意味 3.2.6 論理的帰結と導出 3.3 マルセイユProlog 3.3.1 Prologの記法 3.3.2 Prologの計算規則 3.3.3 Prologプログラムの例 3.3.4 カット・オペレータ 3.3.5 DEC-10 Prologとの相違 3.4 Prolog Ⅱ 3.4.1 difオペレータ 3.4.2 freeze 3.4.3 ループ構造 3.4.4 Prolog Ⅱのインプリメンテーション 3.5 Prolog Ⅲ 3.5.1 制約の枠組 3.5.2 Prolog Ⅲのプログラム例 3.5.3 束縛の領域と制約系 3.5.4 Prolog Ⅲのインプリメンテーション 3.6 まとめ 第4章 制約論理型プログラム (相場 亮) 4.1 はじめに 4.2 制約プログラミング 4.3 制約の分類 4.4 プログラムの実行 4.5 制約の評価 4.6 まとめ 第5章 オブジェクト指向 (柴山悦哉) 5.1 はじめに 5.2 モジュラリティと抽象化 5.2.1 抽象化 5.2.2 手続き抽象 5.2.3 データ抽象 5.2.4 オブジェクトによる抽象化 5.2.5 並列オブジェクトによる抽象化 5.3 共有 5.3.1 多相型 5.3.2 継承 5.3.3 多重継承 5.3.4 Self 5.3.5 動的束縛の意義 5.4 対話性 5.4.1 クラスの再定義 5.4.2 表示機能の一体化 5.5 オブジェクト指向の弱点 5.6 まとめ 第6章 型推論とML (横田一正) 6.1 はじめに 6.2 LCFの超言語からMLへ 6.3 プログラミング言語と型 6.4 MLの表現と型宣言 6.5 MLの型推論 6.6 LCFへの応用 6.7 まとめ 第7章 Miranda (加藤和彦) 7.1 はじめに 7.2 Mirandaの概観 7.2.1 等式による定義 7.2.2 基本データ型と基本演算子 7.2.3 ガード付き等式とスコープ・ルール 7.2.4 高階関数とカリー化 7.2.5 パターン・マッチング 7.2.6 ノンストリクト性と遅延評価 7.2.7 ドット式とZF式 7.3 型 7.3.1 強い型付けと静的な型付け 7.3.2 多相型 7.3.3 型類義 7.3.4 代数データ型 7.3.5 抽象データ型 7.4 処理系 7.5 まとめ 7.6 文献の紹介 第8章 項書換えシステムと完備化手続き (大須賀昭彦) 8.1 はじめに 8.2 項書換えシステム 8.3 TRSの停止性 8.3.1 意味順序 8.3.2 構文順序 8.4 TRSの合流性 8.4.1 完備なTRS 8.4.2 危険対 8.4.3 危険対を用いたTRSの合流性判定 8.5 Knuth-Bendixの完備化手続き 8.6 KBの応用 8.6.1 帰納的な定理証明への応用 8.6.2 等号論理の定理証明への応用 8.7 まとめ 第9章 等式プログラミングから融合型プログラミングへ (富樫 敦) 9.1 はじめに 9.2 等式プログラミング 9.2.1 等式プログラム 9.2.2 代表的な等式プログラム 9.2.3 プログラミング技法 9.2.4 正則プログラムと正規化戦略 9.3 条件付き等式プログラム 9.3.1 条件付き書換え規則 9.3.2 条件の種類 9.3.3 利点と問題点 9.4 融合型プログラミング 9.4.1 AMLOGシステム 9.4.2 向付き等式 9.4.3 実行戦略の変更 9.4.4 代入操作 9.4.5 合流するプログラムへの変換 9.5 まとめ
第1章 有限オートマトン D.Perrin：橋口攻三郎 1. 序論 2. 有限オートマトンと認識可能集合 3. 有理表現 4. Kleeneの定理 5. 星の高さ 6. 星自由集合 7. 特殊なオートマトン 8. 数の認識可能集合 第2章 文脈自由言語 J.Berstel and L.Boasson：富田 悦次 1. 序論 2. 言語 2.1 記法と例 2.2 Hotz 群 2.3 曖昧性と超越性 3. 反復 3.1 反復補題 3.2 交換補題 3.3 退化 4. 非生成元の探求 4.1 準備 4.2 生成元 4.3 非生成元と代入 4.4 非生成元と決定性 4.5 主錐の共通部分 5. 文脈自由群 5.1 文脈自由群 5.2 Cayleyグラフ 5.3 終端 第3章 形式言語とべき級数 A.Salomaa：河原 康雄 1. 序論 2. 準備 3. 書換え系と文法 4. Post正準系 5. Markov系 6. 並列書換え系 7. 射と言語 8. 有理べき級数 9. 代数的べき級数 10. べき級数の応用 第4章 無限の対象上のオートマトン W.Thomas：山崎 秀記 序論 Ⅰ部 無限語上のオートマトン 記法 1. Buchiオートマトン 2. 合同関係と補集合演算 3. 列計算 4. 決定性とMcNaughtonの定理 5. 受理条件とBorelクラス 6. スター自由ω言語と時制論理 7. 文脈自由ω言語 Ⅱ部 無限木上のオートマトン 記法 8. 木オートマトン 9. 空問題と正則木 10. 補集合演算とゲームの決定性 11. 木の単項理論と決定問題 12. Rabin認識可能な集合の分類 12.1 制限された単項2階論理 12.2 Rabin木オートマトンにおける制限 12.3 不動点計算 第5章 グラフ書換え：代数的・論理的アプローチ B.Courcelle：會澤 邦夫 1. 序論 2. 論理言語とグラフの性質 2.1 単純有向グラフの類S 2.2 グラフの類D(A) 2.3 グラフの性質 2.4 1階のグラフの性質 2.5 単項2階のグラフの性質 2.6 2階のグラフの性質 2.7 定理 3. グラフ演算とグラフの表現 3.1 源点付きグラフ 3.2 源点付き超グラフ 3.3 超グラフ上の演算 3.4 超グラフの幅 3.5 導来演算 3.6 超辺置換 3.7 圏における書換え規則 3.8 超グラフ書換え規則 4. 超グラフの文脈自由集合 4.1 超辺置換文法 4.2 HR文法に伴う正規木文法 4.3 超グラフの等式集合 4.4 超グラフの文脈自由集合の性質 5. 超グラフの文脈自由集合の論理的性質 5.1 述語の帰納的集合 5.2 論理構造としての超グラフ 5.3 有限超グラフの可認識集合 6. 禁止小グラフで定義される有限グラフの集合 6.1 小グラフ包含 6.2 木幅と木分解 6.3 比較図 7. 計算量の問題 8. 無限超グラフ 8.1 無限超グラフ表現 8.2 無限超グラフの単項性質 8.3 超グラフにおける等式系 8.4 関手の初期不動点 8.5 超グラフにおける等式系の初期解 8.6 等式的超グラフの単項性質 第6章 書換え系 N.Dershowitz and J.-P.Jouannaud：稲垣 康善，直井 徹 1. 序論 2. 構文論 2.1 項 2.2 等式 2.3 書換え規則 2.4 決定手続き 2.5 書換え系の拡張 3. 意味論 3.1 代数 3.2 始代数 3.3 計算可能代数 4. Church-Rosser性 4.1 合流性 4.2 調和性 5. 停止性 5.1 簡約順序 5.2 単純化順序 5.3 経路順序 5.4 書換え系の組合せ 6. 充足可能性 6.1 構文論的単一化 6.2 意味論的単一化 6.3 ナローイング 7. 危険対 7.1 項書換え 7.2 直交書換え系 7.3 類書換え 7.4 順序付き書換え 7.5 既約な書換え系 8. 完備化 8.1 抽象完備化 8.2 公平性 8.3 完備化の拡張 8.4 順序付き書換え 8.5 機能的定理証明 8.6 1階述語論理の定理証明 9. 書換え概念の拡張 9.1 順序ソート書換え 9.2 条件付き書換え 9.3 優先度付き書換え 9.4 グラフ書換え 第7章 関数型プログラミングとラムダ計算 H.P.Barendregt：横内 寛文 1. 関数型計算モデル 2. ラムダ計算 2.1 変換 2.2 計算可能関数の表現 3. 意味論 3.1 操作的意味論：簡約と戦略 3.2 表示的意味論：ラムダモデル 4. 言語の拡張 4.1 デルタ規則 4.2 型 5. 組合せ子論理と実装手法 5.1 組合せ子論理 5.2 実装の問題 第8章 プログラミング言語における型理論 J.C.Mitchell：林 晋 1. 序論 1.1 概論 1.2 純粋および応用ラムダ計算 2. 関数の型をもつ型付きラムダ計算 2.1 型 2.2 項 2.3 証明系 2.4 意味論と健全性 2.5 再帰的関数論的モデル 2.6 領域理論的モデル 2.7 カルテシアン閉圏 2.8 Kripkeラムダモデル 3. 論理的関係 3.1 はじめに 3.2 作用的構造上の論理的関係 3.3 論理的部分関数と論理的同値関係 3.4 証明論的応用 3.5 表現独立性 3.6 論理的関係の変種 4. 多相型入門 4.1 引数としての型 4.2 可述的な多相的計算系 4.3 非可述的な多相型 4.4 データ抽象と存在型 4.5 型推論入門 4.6 型変数をもつλ→の型推論 4.7 多相的宣言の型推論 4.8 他の型概念 第9章 帰納的な関数型プログラム図式 B.Courcelle：深澤 良彰 1. 序論 2. 準備としての例 3. 基本的な定義 3.1 多ソート代数 3.2 帰納的な関数型プログラム図式 3.3 同値な図式 4. 離散的解釈における操作的意味論 4.1 部分関数と平板な半順序 4.2 離散的解釈 4.3 書換えによる評価 4.4 意味写像 4.5 計算規則 5. 連続的解釈における操作的意味論 5.1 連続代数としての解釈 5.2 有限の極大要素と停止した計算 6. 解釈のクラス 6.1 汎用の解釈 6.2 代表解釈 6.3 解釈の方程式的クラス 6.4 解釈の代数的クラス 7. 最小不動点意味論 7.1 最小で唯一の解を得る不動点理論 7.2 Scottの帰納原理 7.3 Kleeneの列と打切り帰納法 8. プログラム図式の変換 8.1 プログラム図式における同値性の推論 8.2 畳込み，展開，書換え 8.3 制限された畳込み展開 9. 研究の歴史，他の形式のプログラム図式，文献ガイド 9.1 流れ図 9.2 固定された条件をもつ一様な帰納的関数型プログラム図式 9.3 多様な帰納的関数型プログラム図式 9.4 代数的理論 9.5 プログラムの生成と検証に対する応用 第10章 論理プログラミング K.R.Apt：筧 捷彦 1. 序論 1.1 背景 1.2 論文の構成 2. 構文と証明論 2.1 1階言語 2.2 論理プログラム 2.3 代入 2.4 単一化子 2.5 計算過程―SLD溶融 2.6 例 2.7 SLD導出の特性 2.8 反駁手続き―SLD木 3. 意味論 3.1 1階論理の意味論 3.2 SLD溶融の安全性 3.3 Herbrand模型 3.4 直接帰結演算子 3.5 演算子とその不動点 3.6 最小Herbrand模型 3.7 SLD溶融の完全性 3.8 正解代入 3.9 SLD溶融の強安全性 3.10 手続き的解釈と宣言的解釈 4. 計算力 4.1 計算力と定義力 4.2 ULの枚挙可能性 4.3 帰納的関数 4.4 帰納的関数の計算力 4.5 TFの閉包順序数 5. 否定情報 5.1 非単調推論 5.2 閉世界仮説 5.3 失敗即否定規則 5.4 有限的失敗の特徴付け 5.5 プログラムの完備化 5.6 完備化の模型 5.7 失敗即否定規則の安全性 5.8 失敗即否定規則の完全性 5.9 等号公理と恒等 5.10 まとめ 6. 一般目標 6.1 SLDNF-溶融 6.2 SLDNF-導出の安全性 6.3 はまり 6.4 SLDNF-溶融の限定的な完全性 6.5 許容性 7. 層状プログラム 7.1 準備 7.2 層別 7.3 非単調演算子とその不動点 7.4 層状プログラムの意味論 7.5 完全模型意味論 8. 関連事項 8.1 一般プログラム 8.2 他の方法 8.3 演繹的データベース 8.4 PROLOG 8.5 論理プログラミングと関数プログラミングの統合 8.6 人工知能への応用 第11章 表示的意味論 P.D.Mosses：山田 眞市 1. 序論 2. 構文論 2.1 具象構文論 2.2 抽象構文 2.3 文脈依存構文 3. 意味論 3.1 表示的意味論 3.2 意味関数 3.3 記法の慣例 4. 領域 4.1 領域の構造 4.2 領域の記法 4.3 記法上の約束事 5. 意味の記述法 5.1 リテラル 5.2 式 5.3 定数宣言 5.4 関数の抽象 5.5 変数宣言 5.6 文 5.7 手続き抽象 5.8 プログラム 5.9 非決定性 5.10 並行性 6. 文献ノート 6.1 発展 6.2 解説 6.3 変形 第12章 意味領域 C.A.Gunter and D.S.Scott：山田 眞市 1. 序論 2. 関数の帰納的定義 2.1 cpoと不動点定理 2.2 不動点定理の応用 2.3 一様性 3. エフェクティブに表現した領域 3.1 正規部分posetと射影 3.2 エフェクティブに表現した領域 4. 作用素と関数 4.1 積 4.2 Churchのラムダ記法 4.3 破砕積 4.4 和と引上げ 4.5 同形と閉包性 5. べき領域 5.1 直観的説明 5.2 形式的定義 5.3 普遍性と閉包性 6. 双有限領域 6.1 Poltkin順序 6.2 閉包性 7. 領域の帰納的定義 7.1 閉包を使う領域方程式の解法 7.2 無型ラムダ記法のモデル 7.3 射影を使う領域方程式の解法 7.4 双有限領域上の作用素の表現 第13章 代数的仕様 M.Wirsing：稲垣 康善，坂部 俊樹 1. 序論 2. 抽象データ型 2.1 シグニチャと項 2.2 代数と計算構造 2.3 抽象データ型 2.4 抽象データ型の計算可能性 3. 代数的仕様 3.1 論理式と理論 3.2 代数的仕様とその意味論 3.3 他の意味論的理解 4. 単純仕様 4.1 束と存在定理 4.2 単純仕様の表現能力 5. 隠蔽関数と構成子をもつ仕様 5.1 構文と意味論 5.2 束と存在定理 5.3 隠蔽記号と構成子をもつ仕様の表現能力 5.4 階層的仕様 6. 構造化仕様 6.1 構造化仕様の意味論 6.2 隠蔽関数のない構造化仕様 6.3 構成演算 6.4 拡張 6.5 観測的抽象化 6.6 構造化仕様の代数 7. パラメータ化仕様 7.1 型付きラムダ計算によるアプローチ 7.2 プッシュアウトアプローチ 8. 実現 8.1 詳細化による実現 8.2 他の実現概念 8.3 パラメータ化された構成子実現と抽象化子実現 8.4 実行可能仕様 9. 仕様記述言語 9.1 CLEAR 9.2 OBJ2 9.3 ASL 9.4 Larch 9.5 その他の仕様記述言語 第14章 プログラムの論理 D.Kozen and J.Tiuryn：西村 泰一，近藤 通朗 1. 序論 1.1 状態，入出力関係，軌跡 1.2 外的論理，内的論理 1.3 歴史ノート 2. 命題動的論理 2.1 基本的定義 2.2 PDLに対する演繹体系 2.3 基本的性質 2.4 有限モデル特性 2.5 演繹的完全性 2.6 PDLの充足可能性問題の計算量 2.7 PDLの変形種 3. 1階の動的論理 3.1 構文論 3.2 意味論 3.3 計算量 3.4 演繹体系 3.5 表現力 3.6 操作的vs.公理的意味論 3.7 他のプログラミング言語 4. 他のアプローチ 4.1 超準動的論理 4.2 アルゴリズム的論理 4.3 有効的定義の論理 4.4 時制論理 第15章 プログラム証明のための手法と論理 P.Cousot：細野 千春，富田 康治 1. 序論 1.1 Hoareの萌芽的な論文の解説 1.2 C.A.R.HoareによるHoare論理のその後の研究 1.3 プログラムに関する推論を行うための手法に関するC.A.R.Hoareによるその後の研究 1.4 Hoare論理の概観 1.5 要約 1.6 この概観を読むためのヒント 2. 論理的，集合論的，順序論的記法 3. プログラミング言語の構文論と意味論 3.1 構文論 3.2 操作的意味論 3.3 関係的意味論 4. 命令の部分正当性 5. Floyd-Naurの部分正当性証明手法とその同値な変形 5.1 Floyd-Naurの手法による部分正当性の証明の例 5.2 段階的なFloyd-Naurの部分正当性証明手法 5.3 合成的なFloyd-Naurの部分正当性証明手法 5.4 Floyd-Naurの部分正当性の段階的な証明と合成的な証明の同値性 5.5 Floyd-Naurの部分正当性証明手法の変形 6. ライブネスの証明手法 6.1 実行トレース 6.2 全正当性 6.3 整礎関係，整列集合，順序数 6.4 Floydの整礎集合法による停止性の証明 6.5 ライブネス 6.6 Floydの全正当性の証明手法からライブネスへの一般化 6.7 Burstallの全正当性証明手法とその一般化 7. Hoare論理 7.1 意味論的な観点から見たHoare論理 7.2 構文論的な観点から見たHoare論理 7.3 Hoare論理の意味論 7.4 構文論と意味論の間の関係：Hoare論理の健全性と完全性の問題 8. Hoare論理の補足 8.1 データ構造 8.2 手続き 8.3 未定義 8.4 別名と副作用 8.5 ブロック構造の局所変数 8.6 goto文 8.7 （副作用のある）関数と式 8.8 コルーチン 8.9 並行プログラム 8.10 全正当性 8.11 プログラム検証の例 8.12 プログラムに対して1階論理を拡張した他の論理 第16章 様相論理と時間論理 E.A.Emerson：志村 立矢 1. 序論 2. 時間論理の分類 2.1 命題論理 対 1階述語論理 2.2 大域的と合成的 2.3 分岐的 対 線形 2.4 時点と時区間 2.5 離散 対 連続 2.6 過去時制 対 未来時制 3. 線形時間論理の技術的基礎 3.1 タイムライン 3.2 命題線形時間論理 3.3 1階の線形時間論理 4. 分岐的時間論理の技術的基礎 4.1 樹状構造 4.2 命題分岐的時間論理 4.3 1階の分岐的時間論理 5. 並行計算：その基礎 5.1 非決定性と公平性による並列性のモデル化 5.2 並列計算の抽象モデル 5.3 並列計算の具体的なモデル 5.4 並列計算の枠組みと時間論理の結び付き 6. 理論的見地からの時間論理 6.1 表現可能性 6.2 命題時間論理の決定手続き 6.3 演繹体系 6.4 モデル性の判定 6.5 無限の対象の上のオートマトン 7. 時間論理のプログラムの検証への応用 7.1 並行プログラムの正当性に関する性質 7.2 並行プログラムの検証：証明論的方法 7.3 時間論理による仕様からの並行プログラムの機械合成 7.4 有限状態並行システムの自動検証 8. 計算機科学における他の様相論理と時間論理 8.1 古典様相論理 8.2 命題動的論理 8.3 確率論理 8.4 不動点論理 8.5 知識 第17章 関係データベース理論の構成要素 P.C.Kanellakis：鈴木 晋 1. 序論 1.1 動機と歴史 1.2 内容についての案内 2. 関係データモデル 2.1 関係代数と関係従属性 2.2 なぜ関係代数か 2.3 なぜ関係従属性か 2.4 超グラフとデータベーススキーマの構文について 2.5 論理とデータベースの意味について 3. 従属性とデータベーススキーマ設計 3.1 従属性の分類 3.2 データベーススキーマ設計 4. 問合わせデータベース論理プログラム 4.1 問合わせの分類 4.2 データベース論理プログラム 4.3 問合わせ言語と複合オブジェクトデータモデル 5. 議論：関係データベース理論のその他の話題 5.1 不完全情報の問題 5.2 データベース更新の問題 6. 結論 第18章 分散計算：モデルと手法 L.Lamport and N.Lynch：山下 雅史 1. 分散計算とは何か 2. 分散システムのモデル 2.1 メッセージ伝達モデル 2.2 それ以外のモデル 2.3 基礎的概念 3. 分散アルゴリズムの理解 3.1 挙動の集合としてのシステム 3.2 安全性と活性 3.3 システムの記述 3.4 主張に基づく理解 3.5 アルゴリズムの導出 3.6 仕様記述 4. 典型的な分散アルゴリズム 4.1 共有変数アルゴリズム 4.2 分散合意 4.3 ネットワークアルゴリズム 4.4 データベースにおける並行性制御 第19章 並行プロセスの操作的および代数的意味論 R.Milner：稲垣 康善，結縁 祥治 1. 序論 2. 基本言語 2.1 構文および記法 2.2 操作的意味論 2.3 導出木と遷移グラフ 2.4 ソート 2.5 フローグラフ 2.6 拡張言語 2.7 その他の動作式の構成 3. プロセスの強合同関係 3.1 議論 3.2 強双模倣関係 3.3 等式による強合同関係の性質 3.4 強合同関係における置換え可能性 3.5 強等価関係上での不動点の唯一性 4. プロセスの観測合同関係 4.1 観測等価性 4.2 双模倣関係 4.3 観測合同関係 4.4 プロセス等価性上での不動点の唯一性 4.5 等式規則の完全性 4.6 プロセスの等価性に対するその他の概念 5. 双模倣等価関係の解析 5.1 等価性の階層構造 5.2 階層構造の論理的特性化 6. 合流性をもつプロセス 6.1 決定性 6.2 合流性 6.3 合流性を保存する構成子 7. 関連する重要な文献
via Twitterオタが非オタの彼女にTwitter世界を軽く紹介するための10ユーザ
まあ、どのくらいの数のプログラミング言語オタがそういう彼女をゲットできるかは別にして、
「オタではまったくないんだが、しかし自分のオタ趣味を肯定的に黙認してくれて、
その上で全く知らないプログラミング言語の世界とはなんなのか、ちょっとだけ好奇心持ってる」
ような、ヲタの都合のいい妄想の中に出てきそうな彼女に、プログラミング言語のことを紹介するために
習得させるべき10言語を選んでみたいのだけれど。
（要は「脱オタクファッションガイド」の正反対版だな。彼女にプログラミングを布教するのではなく
相互のコミュニケーションの入口として）
あくまで「入口」なので、アーキテクチャに過度に依存するアセンブラ等の低級言語は避けたい。
あと、いくら基礎といってもBrainf*ckやUnlambdaのような難しすぎるものは避けたい。
ポール・グラハムが『Arc』は外せないと言っても、それはちょっとさすがになあ、と思う。
そういう感じ。
彼女の設定は
ロジカル度が高く、頭はけっこう良い
まあ、いきなりここかよとも思うけれど、「Java以前」を濃縮しきっていて、「Java以後」を決定づけたという点では
ただ、ここでオタトーク全開にしてしまうと、彼女との関係が崩れるかも。
この情報過多な言語について、どれだけさらりと、嫌味にならず濃すぎず、それでいて必要最小限の情報を彼女に
伝えられるかということは、オタ側の「真のコミュニケーション能力」の試験としてはいいタスクだろうと思う。
アレって典型的な「オタクが考える一般人に受け入れられそうなプログラミング言語（そうオタクが思い込んでいるだけ。実際は全然受け入れられない）」そのものという意見には半分賛成・半分反対なのだけれど、それを彼女にぶつけて確かめてみるには一番よさそうな素材なんじゃないのかな。
「プログラミング言語オタとしてはこの二つは“教育用言語”としていいと思うんだけど、率直に言ってどう？」って。
ある種の言語オタが持ってるラムダ計算への憧憬と、ACM監修の関数型言語的純粋さへのこだわりを
彼女に紹介するという意味ではいいなと思うのと、それに加えていかにも参照透過な
の二要素をはじめとして、オタ好きのする要素を言語にちりばめているのが、紹介してみたい理由。
たぶんこれを見た彼女は「Emacsだよね」と言ってくれるかもしれないが、そこが狙いといえば狙い。
この系譜の作品がその後続いていないこと、これがポール・グラハムの間では大人気になったこと、
ポールグラハムがウェブサービスの構築に使って、それがいろんなウェブサービス開発者にも影響しててもおかしくはなさそうなのに、
実際のウェブサービスでこういうのが使われないこと、なんかを非オタ彼女と話してみたいかな、という妄想的願望。
「やっぱりプログラミングはバッチ処理のためのものだよね」という話になったときに、そこで選ぶのは「awk」
でもいいのだけれど、そこでこっちを選んだのは、この言語にかけるラリーとdankogaiの思いが好きだから。
断腸の思いで延ばしに延ばしてそれでも2008年、っていうPerl 6のリリース予定日が、どうしても俺の心をつかんでしまうのは、
そのリリースというイベントへの諦めきれなさがいかにもオタ的だなあと思えてしまうから。
Perlのリリース延期を無駄だとは思わないし、拙速なリリースは無茶だろうとは思うけれど、一方でこれが
GuidoやMatzだったらきっちり予定通りリリースしてしまうだろうとも思う。
なのに、各所に頭下げて迷惑かけてリリースを延期してしまう、というあたり、どうしても
「自分の言語を形作ってきた哲学(TMTOWTDI)が捨てられないオタク」としては、たとえラリーがそういうキャラでなかったとしても、
親近感を禁じ得ない。言語自体の高評価と合わせて、そんなことを彼女に話してみたい。
今の若年層でPostscriptを直で書いたことのある人はそんなにいないと思うのだけれど、だから紹介してみたい。
PDFよりも前の段階で、DTPの哲学とか印刷技法とかはこの作品で頂点に達していたとも言えて、
こういうクオリティのプログラミング言語がエディタで書かれてたんだよ、というのは、
別に俺自身がなんらそこに貢献してなくとも、なんとなくプログラミング言語好きとしては不思議に誇らしいし、
いわゆるJava VMでしかスタック型言語を知らない彼女には見せてあげたいなと思う。
PHPの「HTMLに埋め込み可能な点」あるいは「RDBMSとの接続性」をオタとして教えたい、というお節介焼きから教える、ということではなくて。
「HTMLのテンプレートエンジンを作り続ける」的な感覚が言語オタには共通してあるのかなということを感じていて、
だからこそアメリカ版『Yahoo!』の開発言語はPHP以外ではあり得なかったとも思う。
「MとVとCを分離なんてできない」というオタの感覚が今日さらに強まっているとするなら、その「オタクの気分」の
源はPHPにあったんじゃないか、という、そんな理屈はかけらも口にせずに、
単純に楽しんでもらえるかどうかを見てみたい。
これは地雷だよなあ。地雷が火を噴くか否か、そこのスリルを味わってみたいなあ。
こういう述語論理風味の計算をこういうかたちで言語化して、それが非オタに受け入れられるか
気持ち悪さを誘発するか、というのを見てみたい。
9本まではあっさり決まったんだけど10本目は空白でもいいかな、などと思いつつ、便宜的にC++を選んだ。
Javaから始まってC++で終わるのもそれなりに収まりはいいだろうし、テンプレート以降のメタプログラミング時代
の先駆けとなった言語でもあるし、紹介する価値はあるのだろうけど、もっと他にいい言語がありそうな気もする。
というわけで、俺のこういう意図にそって、もっといい10本目はこんなのどうよ、というのがあったら
教えてください。
「駄目だこの増田は。俺がちゃんとしたリストを作ってやる」というのは大歓迎。
こういう試みそのものに関する意見も聞けたら嬉しい。
