  |
はてなキーワード: 型推論とは
いわゆる「LL」ではないけど、Scalaを挙げておきたい。希望の要件はおおむね満たしてると思うけど、以下注釈。
val users = service.getUsers // 1 val result = users.map { users ＝＞ users.filter { u ＝＞ u.name.head == 'T' // 2 }}.flatMap { users ＝＞ Future.traverse(users) { user ＝＞ db.write(user.id, user.name) // 3 }} result.onSuccess { case _ ＝＞ println("Success!") // 4 } // '＝＞'がうまく書けなかったので全角になってる。
普段Perlを書いているんだけど、言語機能として欲しい機能がライブラリ任せだったりしていろいろしんどい。
何かいいプログラミング言語はないかなーと思っているんだけど、なかなか自分の好みとピタリとくるものがない。まぁ好みにピタリとくるものなんかプログラミング言語に限らずないんだろうけど。
なので夢想してたのを垂れ流してみる。最近OOPディスのエントリとかあったので話題作りになれば。
Web系のエンジニアなのでWebサービス作ることが前提で、範囲広げすぎるとまとまらないので今回はLLを想定してる。
だいたい PHP, Perl, Python, Ruby, JavaScript あたりをイメージしながら、さらにこんな機能があればいいなーと思って書いたよ。
あ、まず前提として、
はたして貴女を幸福にするかどうか、それはまた別問題だけれど。
ＩＴ系の超かしこい男なども多く、
多くっつーかIT系でないのにプログラミング大好き男っていうのは超かしこい学生（まぁこれは有望株）か研究者系なんか、
あとはまったくかしこくもないクセに頭いいつもりして「Lispやってます（ｷﾘｯ ハローワールドくらいですが」とか言っちゃうアホしかいないわけで、
したがって、釣り師たる女たちにとっては、
なかなかあなどれない釣り場です。
では、プログラミング大好き男に「どの言語が好き？」と訊ねられたとき、
まず最初に、その男がCOBOLのようなタイプのレガシーコードと
あとはC/C++、そして（TechEdに参加するほどではないけれど）VisualBasicが大好きな、
貴女はかれの目を見て、微笑みとともに質問など無視して、こう言いましょう、
「わたしが、仕様書を作ってあげる♪」
これこそまさに必殺の答えです。
そこでプログラミング大好き男が、えへへ、とやにさがったならば、
貴女は、ひそかに、「コピペ量産しやすい技術的ポイントを抑えた仕様書」あたりを
ひそかに練習しておきましょう。これで成功まちがいなしです。
しかし、ここでは、もう少しハイブロウな（？）いわゆるプログラミング好きの男の
落とし方をお伝えしましょう。
「わたしは、JVM上のScalaが好き。
型推論もあるしラムダ式やクロージャもスクリプト言語みたいに書けるの、豊富な組み込みのコレクションメソッドはいつも便利だし、
XMLリテラルもCaseクラスによるパターンマッチもTraitベースのMixi-inも、大好き♪」
もしも貴女がそう答えたならば、
かれの貴女への恋心は、
２０％増量になるでしょう。
なぜって、Scalaは、
コンパイルは遅いながらも、そこがまた
ちょっぴりメモリを多く積めばいい富豪プログラミングみたいなふんいきをかもしだしていて。
質高くふるまっていて、なおかつ、
JVM上で動くくせにJavaが「やるやる」と言ったまま実装してなかったラムダ式と仮想拡張メソッド、型推論を実装した功績もあって。
したがってScalaこそは、
本来なんの接点もないまったく縁もゆかりもない別々の世界に生きている、
インタプリタ言語大好きな綺麗系ＯＬと、玉もあれば石も混じっている、そんなプログラミング大好き男たちが、
この世界で唯一（いいえ、JVM系列のJRuby、Clojure と並んで唯三）遭遇しうる場所です。
●
では、参考までに、危険な回答を挙げておきましょう。
プログラミング大好き男に「どの言語が好き？」と訊ねられたとき、
「MicrosoftのVisual Basic for Applicationが好き♪ 週３回は Excelでコーディングするの。」
特にOfficeは平凡ながら、ま、無難にまとめてあるものの、
しかし、「新UIのリボンUI！」「メトロUI対応！」とかなんとか無意味な自慢を吹聴し、
VBAはさらにプログラミングについての謬見を撒き散らした罪がありますから、プログラミング大好き男にとっては天敵なんです。
ティーガー戦車乗りのオットー・カリウスは「ティーガー乗りなら誰でも片側の履帯がはずれ僚車に牽引されて帰ってきた経験を持つはずだ」 って言ったけど
社内SEかSIerなら誰でもクソみたいな前任者が書いたクソみたいなExcel-VBAコードを直した経験があるはずなんです。
また、もしも貴女が「PHPが大好き♪ あたしが書いたPHPのWebサイトが、さくらサーバに７件あるよ♪」
と答えたとしても、同様の効果をもたらすでしょう、
なぜって、PHPは、１９９０年代にはWeb系を目指す人にとっては簡単で要件を満たすWebサイトが簡単に作れる輝きの道だったものの、
しかし２０００年代そうそうから、セキュリティ関係の問題で転落し、
いまや、あの貧弱な言語能力では、Rubyの魅力に遥かに及びません。
（注１）
「わたし、.NET FrameworkのC#が好き、フォームアプリでも書くけど、
最高に好きなのはASP.net♪ SQLServer連携も、ajax control toolkitもすっごくおいしいの。」
と、答えたとしたらどうでしょう？
なるほど、貴女の趣味は高く、
たしかに.NET Frameworkは、C# が cool であるのみならず、
.NET Framework上で動く F# や IronPythonやIronRuby、マネージJScriptも最高においしいんですけれど、
しかし、貴女の答えを聞いて、プログラミング大好き男はきっとおもうでしょう、
（なんだよ、MS信者な女だな、カネかかりそう）って。
（注２）
貴女が、プログラミングが大好きで、言語の名を挙げるにしても、
たとえば、JavaScript(node.js)ならば安心でしょう、
なぜならば、JavaScriptは、かけだしのプログラミング初心者にもマニアにもともに愛されるめずらしい言語で、
貴女がその名前を挙げても必ずしも、(jQueryがやっとの初心者と思われることはあっても)あなたがプログラミング言語おた宣言をしているとは受け取られないでしょう。
むしろ「へぇ。ちゃんとprototypeは使ってる？」と聞かれたら「当たり前じゃない。むしろnode.jsでいいMVCフレームワークが分からないんだけど…」と話を振ってみましょう。
男は嬉々として、３０個くらいのnode.jsのフレームワークを教えてくれることでしょう。（まぁどれもどれで帯に短し襷に長しなんですが）
あるいはRighno上で動かしたコードをnodeへ移植する話とか、CoffeeScript、甚だしきはClojureScriptを振ってみてもいいかもしれません。
しかし、たとえば、世界が（つーか竹内先生とポール・グレアムが）誇る超絶関数型言語の名作、Common Lispにせよ、
selfと書きまくることと海外で使われてることに定評のあるPythonにせよ、
バージョンアップごとに言語仕様が変わり、かなり素敵なものではあるもののobsolatedな罠にはまりやすいRubyにせよ、
まったく読めない$_だらけで頭悪い仕様をリセットしてPerl6にする（そしてまた全く読めない）Perlにせよ、
気さくなクジラ飛行机さんがふるまう素敵においしい日本語プログラミング言語のひまわり・なでしこにせよ、
基地外トリッキー言語の代表BrainFxck・Glass・Missa・WhiteSpaceにせよ、
ましてや貴女が、「Haskellが大好き♪ わたし、プロジェクト・オイラーの問題もうほとんどHaskellで、解いちゃった♪」
と答えたならば、どうでしょう？
これはかなり博打な答え方で、
なるほど、Haskellは、純粋関数型でありつつも副作用のある操作が行える超絶名言語ゆえ、
あなたがそう答えた瞬間、プログラミング大好き男がいきなり超笑顔になって、
「へぇ、やっぱりHaskellなら大抵の問題は４行以内くらいで解いちゃった？」とか言いながら
鼻の下がだら～んと伸びちゃう可能性もあるにはありますが、
しかし、逆に、（なんだよ、この女、プログラミングおたくかよ）とおもわれて、どん引きされる可能性もまた大です、
なぜって、必ずしもプログラミング大好き男がプログラミング大好き女を好きになるとは、限らないですから。
男たちは、女を導き高みへ引き上げてあげることが大好きゆえ、
もしも貴女が、「Haskellが大好き♪」なんて言ってしまうと、
そこにはもはや、男が貴女に圏論のモナドを教育する余地がまったく残されていません、
したがって貴女のその答えは、
プログラミング大好き男の貴女への夢を潰してしまうことに他なりません。
ま、ざっとそんな感じです、貴女の目にはプログラマーたちはバカでスケベで鈍感に見えるでしょうが、
しかし、ああ見せて、プログラマーはプログラマーで繊細で、おざなりに扱われると傷つきやすく、ローカル変数の名前一つにも気を使い、女と自分の将来に夢を持っています、
貴女の答え方ひとつで、プログラマーの貴女への夢は大きくふくらみもすれば、
一瞬で、しぼんでしまいもするでしょう。
●
では、スキットを繰り返しましょう。
「わたしは、JVM上のScalaが好き。
型推論もあるしラムダ式やクロージャもスクリプト言語みたいに書けるの、豊富な組み込みのコレクションメソッドはいつも便利だし、
XMLリテラルもCaseクラスによるパターンマッチもTraitベースのMixi-inも、大好き♪」
そして、その瞬間、プログラミング大好き男の目がらんらんと輝いたなら、
貴女はこう重ねましょう、
「それからね、いま、わたしが使ってみたいWebアーキテクチャは、
Play Framework、素敵なリアルタイム嗜好のアーキテクチャって噂を聞いたから。
あなたのお暇なときがあったら、わたしをPlayへ連れてって♪」
これでもう完璧です。
PlayFrameworkと、Play（遊ぶ・じゃれる）のダブルミーニングでかれの股間も刺激しちゃえます。
そうなったらこっちのもの、
デートの日には、ペアプロ用に Happy Hacking Keyboard をばっちり決めて、かわいい下着をつけて（注３）、
github.comの通販で売ってるoctcatのTシャツか、facebookの「いいね！」ボタンがムネのところにあるTシャツ、 あるいは初音ミク（ないし彼のお気に入りのアニメキャラ。北米ならMyLittlePonyで鉄板なんだけど）のコスプレを着てゆきましょう。
その日から、プログラミング大好き男は貴女の虜になるでしょう。
注１：
（と、書いたもののPHPの現状をよく知りません。グローバル変数だらけになるのとか旧ASPみたいなもんなのかなぁ。count($array); とか書くのアホと思うがpythonも同じだった）
（あと、マジで単機能とかTwitter連携とか診断メーカー的なのでもPHPで７つも作ってる女子居たら付き合いたい）
注２：
もっとも。objective-Cなんていう言語をやることに比べれば個人で行う程度なら金のかからない手法もなくはないのですが。
注３：
プログラマーにとっての「かわいい下着」と、女性にとっての「かわいい下着」の定義にずれがあるので注意。
半数くらいのプログラマーはしましまぱんつが可愛いと思ってる気がするので、妙齢の女性が着用するには抵抗あると思うが、ボーダー柄のコットンショーツ（ただしキャラ絵のは除く）とか、
過度でないていどにフリルがついたものがオススメ。また、色は、レッドだとプログラミング大好き男は引いてしまう（だってそれはコンパイルエラーのときの色だ）ので、薄ピンクかホワイト、薄ブルー、せめて黒（に差し色でピンクとか）あたりに留めたい。
補記：
元ネタ： http://tabelog.com/tokyo/A1301/A130101/13002457/dtlrvwlst/3464106/
補記２：
「プログラマー」か「プログラマ」かの問題については、特に意味は無いが前者を採用した。
補記３：
言うまでも無いけど、ネタです。
いっせーの! Webにのって さあ出かけよう ブラウザとのランデブー ユーザーが大事 実装が大事 JS、マジ大好き ユーザーの痛み それ言語のせい? UIの動き UXのつもり 今までのJSのポジションを 越えた未来は どうなるの? ねぇどうせWebKitでしよ ダメ? ダメ! ECMA標準だけ 油断も隙もない APIとのボーダー越えたい そうもっと! 大胆で ちょっと強引? 俺ワールド全開 優しいJSも いじわるなJSも ひとりじめ 型つけてみて やっぱやめて ウラハラ alt-js Java以上C++未満の JS、マジ最高 V8だけが きらめいて 遠い背中も 追いかけたよ これからの最適化 フローグラフの分まで伝えたい ぎゅってしてPNaClコンパイル ダメ? ダメ! 不埒です CSS3に甘えたい GPUに触れたい どこまで? APIのボーダー教えて おっとっと! 手強い IEの仇 ムキになったら 古いシステムも Flashの将来も 譲れない 実装して やっぱやめて 一方通行プロセス W3C信じて プラグイン書いて No more E4X 動的なの? 静的なの? 型推論好き? 好き! 好きだから 笑わず答えて Ion Monkey 越えよう おっとっと! 大胆で ちょっと強引? prototypeを知ったら JSでの設計や コーディングも変わるの? 答えてよ! ときめき 走り出す わくわくコーディング Self以上 Scheme未満の JS、超愛してる!!
元記事はそんなに外してもいないと思いますけどね。
静的型付き言語として関数型言語を持ち出してくるのは、論点が違うような気がしました。
静的型、型推論の嬉しさって、関数が一級かどうかでも違ってくると思いますし。
(つまり、静的型の得失について、scheme vs ML での議論と Java vs Perl の議論は別物だと思います)
結局は適材適所という結論にしかならないと思いますが、たとえば Web 系なら静的型付き言語で書いても面倒臭さの方が多そうです。
Web 系で一番面倒なのは文字列の扱いなので。そこは型システムで何も解決しないですよね。
そういうことより、文字列を関数名として $funcName(arg1, arg2) みたいにコールできたりとか、
そういう柔軟さが便利なのですよね。
こういうの、静的型がある言語だと大変ですよね。Java ならリフレクションですよね。
他の言語ではどうするのでしょう。おそらく、自前で関数テーブルを作ることになるでしょうか。
静的型を持たない言語での開発が、大規模になると破綻するというようなことが言われます。
大規模開発といっても、大抵フレームワークの規約に沿って実装するだけですし、
規模を LOC だと考える限りにおいては、大規模になっても複雑さは LOC に比例しませんから。
単純にモジュール数が増えるだけで、一つ一つは単純な実装の繰り返しですよね。
おさしみにたんぽぽを乗せるお仕事と変わりません。たんぽぽの山が積まれていて途方に暮れるだけです。
もちろん、大規模になったときにスケールしなくなるので C/Java にするというのはありますけど。
静的型言語の課題は、十分強力な型推論を持ってる言語が実用プログラムを書くのにパラダイムシフトを要求する点なんだが、それよりなにより「なんだか怖い点」にあると思う。信奉者が「そんなことはない」と熱く否定するさまがますます怖い。
@yukihiro_matz さんは普通のユーザの声を代弁している。@perlcodesample さんが静的型付き言語を使う人々の餌食になったのも記憶に新しい。彼らは何を恐れ、既存のプログラミング言語を使う人々を攻撃し続けるのか。
型理論は先人から積み上げられたすばらしい理論体系だ。きちんと理解できる人は一部のエリートに限られ、こうしたエリート達の努力には本当に頭が下がるばかりだ。しかし、こうしたエリートのやってることは一般の人々からは評価されにくい。今、日本で有名な物理学者は誰か、名前を挙げられる人は居るだろうか。今、世界中の医学者達が力を注いでいるのはどのような研究だろうか。普通の人は答えられない。
彼らは努力している分、人から評価されることを求める。しかし、努力=評価となるほど世の中甘くはない。残念ながら、頭の良さ=評価ともならない。そのため、彼らは普通の言語を使う人々はいかに劣っており、自分たちが時間を費やしてきたことがいかに価値のあることかをアピールするために他者を攻撃する必要が出てくる。そうしなければアイデンティティを保てない。
彼らのやっていることが本当に価値があることならば、そこまで他者を否定しなくとも勝手に支持者が増えていくのではないか。彼らのやっていることが本当に正しいのであれば、静的型付き言語によって成功するプロダクトが幾多も現れ、その効果を自然と証明できるのではないか。彼らは、そうなっていない現状に焦りを感じ、恐れている。本当は静的型付き言語は実用的ではなく、自分たちの苦労は報われないのではないかと。
理論が美しいとか、エリートであるとか、そういうことだけでは必ずしも優遇されないのが社会の実情だ。静的型付き言語を使って、レガシーな命令型言語や動的型付き言語の欠点を暴露するような成果をどんどん出せばよい。
最後に、静的型付き言語の人々が忌み嫌う、動的型付き言語のコミュニティの言葉を送ることでこのエントリを締めくくろう。静的型付き言語で、正しいプログラムからなるきちんとした社会を実現してやろうじゃないか。
Shut the fuck up and write some code.
◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆◆
（追記）
これ、書いたのperlcodesample本人だろ
自演乙。
冤罪とか問題になってるご時世なので念のため言っておくけど、僕は@perlcodesample さんではない。上で下品な言い方をしたのでそこを批判されるのは当然だと思うけれど、言いたかったのは、ソフトウェアの世界は形式手法や型理論が全てではないわけだし、CS的な裏付けのないコード書いてる相手に対して一方的に自分の方が上の立場だと思わずに、もっと相手のやっていることを尊重して話をした方がいいってこと。
変数に型がないということの利点について考える
http://d.hatena.ne.jp/perlcodesample/touch/20130227/1361928810
が大変お粗末な内容だったので、反論記事を書きます。
型推論はソースコードのコンパイルの時間を遅くしてしまいます。ソースコードが大きくなってきた場合に、すばやく書いて、すばやく実行結果をもらうことができなくなります。
大規模開発環境はコンパイル時間よりリンク時間の方が問題になりやすいが、それは別に型の話とは関係ない。
あと、インタープリタも最近は実行時にJITコンパイラが走る。
実行時間に影響がなく、開発者の待ち時間で済む方が実はよいのでは？
統合開発環境での、メソッドの自動補完の機能の実装が少し難しくなります。
みんなが統合開発環境をつくるとでも？
そもそも型が不定なら補完することすらできないので、
比較対象として相応しくない。
変数に型がないとソースコードの変更に強くなります。たとえば右辺の返す型に変更があったとしても、受け取る側のソースコードを変更する必要はありません。
これは逆に危ない。
実行するまで意図したインスタンスが返ってこなくなった事実に気づかないから。
変数の型を持つ言語は、型が異なるのだが、処理としては同一の処理を行いたい場合には、オーバーロードという機能を使う必要があります。変数の型がなければ、オーバーロードの機能は必要ではなく、ただ単にif文で分岐すればよいだけなのでとても楽です。
CならVTable。Javaならinstanceofなど同等の事はできます。
というか、これ。型を意識しまくったコードじゃないですか？？？
C++のテンプレートのような複雑でデバッグしにくい機能を使ったりしなければなりません。
実は全然ちがうものが混ざってた！なんて事故がコンパイラによって止められる分、デバッグする必要すら無いんですけどね。
変数に型がないとどのような型の値が代入されているかわからないという批判があるかと思います。可読性の問題で
第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. 関連する重要な文献
あくまで自分でこう答えるという話。
(問1)
(define fold-left
(lambda (func obj lst)
(cond
((null? lst)
obj)
(else
(fold-left func (func obj (car lst)) (cdr lst))))))
(define my-sum
(lambda (lst)
(fold-left + (car lst) (cdr lst))))
・例
(my-sum '(1 2 3 4 5 6 7 8 9 10))
(問2)
(define fold-left
(lambda (func obj lst)
(cond
((null? lst)
obj)
(else
(fold-left func (func obj (car lst)) (cdr lst))))))
(define large
(lambda (x y)
(cond
((>= x y)
x)
(else
y))))
(define my-max
(lambda (lst)
(fold-left large (car lst) (cdr lst))))
・例
(my-max '(58 90 1 2 4 3 100))
(問3)
(define fold-right
(lambda (func lst obj)
(cond
((null? lst)
obj)
(else
(func (car lst) (fold-right func (cdr lst) obj))))))
(define my-apply
(lambda (func obj)
(func obj)))
(define plus5
(lambda (num)
(+ num 5)))
(define times10
(lambda (num)
(* num 10)))
(define divide2
(lambda (num)
(/ num 2)))
(define plus5-times10-divide2
(lambda (num)
(let ((lst (list plus5 times10 divide2)))
(fold-right my-apply (reverse lst) num))))
・例
(plus5-times10-divide2 5)
全部畳み込み関数を使っているのは、はじめ使い道がないと思ってたのにかなり使い道があることがわかったので、それを示したかったから。あとmap関数あたりはほかの言語でもあるから、すぐに思いつくだろうし。
というか最後のやつは手続きを抽象化することでリストの形で扱えるようにしているから、関数プログラミングでは重要だと思う。関数プログラミングの肝は計算によって手続きを含めたすべて表すことができることだと思っている。その例だと思うんだけどね。例えばSchemeなら上記の答えを応用して、似たような「手続き」を生み出す関数を作ることができる。
(define make-proceduce (lambda (fst . rest) (let ((lst (cons fst rest))) (lambda (num) (fold-right my-apply (reverse lst) num)))))
これを使うと次のようにできる。
(define divide2-plus5-times10
(make-proceduce divide2 plus5 times10))
(divide2-plus5-times10 2)
(define divide2-times10-plus5
(make-proceduce divide2 times10 plus5))
(divide2-times10-plus5 2)
関数合成がつかえるならそっちのほうが楽だけど、リストという形で「手続き」をつくり出していることがわかるだろうか？手続きをリストで操作できるのだ。こういうのが関数プログラミングの肝だと勝手に思っている。
こうやってくると型推論や多相型の重要性もわかると思うんだよ。上記のようなことはPythonでもできる。でも高階関数はつかいすぎるとわかりにくい。どっかにバグが入ってくるかもしれない。それを機械的に防ぐのが型推論。型という観点から型推論でおかしいところを探し出してくれる。それならC言語でもいいのではないかという人もいるかもしれない。だがC言語は融通が利かない。例えばapply関数にしても引数の型が数値なら数値、文字なら文字と決まっている必要がある。だから数値に向けにapply関数を作っても文字には使えない。こうした型のデメリットをなくす一方、そのメリットを享受するためにあるのが多相型。これによってapply関数やmap関数を一般的に作ることができ、型のメリットを享受しながらデメリットをなくすことができる。このように関数で手続きなんかを抽象化するときに型推論や多相型があると便利なのだ。
getter/setterを関数で書くと、後ろに()を付けないといけないから格好悪い！！
って人にオススメ？
template<typename T>struct _property{
virtual operator T() = 0;
typedef T _t;
};
class asdf{
int foo;
public:
struct __foo : _property<int>{
asdf &parent;
operator _t(){
printf("親クラス（？）のメンバへのアクセスが面倒...");
return parent.foo;
}
__foo(asdf &p) : parent(p){}
}y;
struct : _property<char*>{
operator _t(){
printf("ここに副作用付き処理を書ける！？\n");
printf("この関数が参照を返せばgetもどきも実装できる！？\n");
return "ふひひひ！やったね！！";
}
}x;
asdf(int v) : y(*this){ foo = v * v - v - v; }
};
void p(char*s){ printf("\n増田はこちらを振り返ると、\n悲しそうな顔をしてこう言った\n「%s」\n", s); }
int main(){
asdf a(127);
//生でprintfに渡すと型推論が行われない
//それ以外の関数だったら問題ないかも
p(a.x);
printf("\n");
//どうしてもと言うならキャストすべし
printf("\n%d\n", (int)a.y);
return 0;
}
VC8で動作確認してるよ！
はっきり言って普通にgetter/setter書くよりも手間多いね！