Last active
August 29, 2015 14:21
-
-
Save takada-at/541581a8660d2f643c78 to your computer and use it in GitHub Desktop.
SEP「計算機科学の哲学」
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
http://plato.stanford.edu/entries/computer-science/ | |
-計算機科学の哲学(PCS)は、計算機科学の本質と実践に対する反省から生じた哲学的トピックを扱う。 | |
-計算機科学の実践というのは単に「プログラミング」のことではない。 | |
--プログラミング自体は物理とか化学とか他の分野の人もする。 | |
-計算機科学はむしろ計算機にかかわる概念や方法論の設計・開発・研究にかかわるメタな活動だ。 | |
--たとえば | |
--プログラムのデザインと分析 | |
--言語の仕様記述とアーキテクチャーの記述 | |
--コンパイラ、インタープリタ、定理証明器、型推論システムの構築と最適化 | |
--ロジカルフレームワークの考案や組み込みシステムの設計 | |
--など | |
-計算機科学の哲学における問題の多くはこうした活動にかかわっている。 | |
-多くは、こうした活動にかかわる論理学的、存在論的、認識論的問題だ。 | |
-しかし、「計算機科学とは計算機科学者がする研究である」という以上に計算機科学の定義を考えるのはむずかしい。 | |
--むしろ「PCS(計算機科学の哲学)が計算機科学の本質を理解するのに役立ちますように!」ということこそこの記事の目的だから、ここでこれ以上定義を論じても仕方ない。 | |
*1* 1.中心的トピックのいくつか | |
いきなり中心的トピックを列挙してみるよ! | |
+プログラムって何?プログラムは抽象物なのか具体物なのか?(Moor 1978; Colburn 2004) | |
+プログラムとアルゴリズムのちがいは?(Rapaport 2005a) | |
+仕様って何?仕様が定義されているってどういうこと?(Smith 1985; Turner 2005) | |
+仕様とプログラムは根本的にちがうものなのか?(Smith 1985) | |
+実装って何?(Rapaport 2005b) | |
+何がハードウェアをソフトウェアから区別するの?プログラムは物理的にも存在するし、記号的な形式としても存在するのか?(Moor 1978; | |
Colburn 2004) | |
+デジタルな対象って何? デジタルな対象のために新しい存在論的カテゴリーを導入する必要はあるのか?(Allison et al. 2005) | |
+プログラミング言語のいろいろな意味論的理論の目的は何?(White 2004; Turner 2007) | |
+プログラミング言語の哲学における諸問題は、言語哲学における対応する諸問題とどういう風にかかわっているのか?(White 2004) | |
+モジュラリティの原理*(e.g., Dijkstra 1968)は、full-abstractionや合成性といった概念的問題に関係するのか? | |
+「構造化プログラミング、関数型プログラミング、論理型プログラミング、オブジェクト志向プログラミング」といったプログラミングのパラダイムの間には、どういう概念的なちがいがあるのか? | |
+計算機科学におけるタイプの役割って何?(Barandregt 1992; Pierce 2002) | |
+操作的意味論と表示的意味論のちがいは何?(Turner 2007) | |
+プログラムが「正当である」ってどういうこと? 正当性の証明の認識論的地位はどうなってるの? | |
これは数学における証明と根本的にちがうものなのか?(DeMillo et al. 1979; Smith 1985) | |
+(プログラムの)正当性の証明は何を達成しているのか?(Fetzer 1988; Fetzer 1999; Colburn 2004) | |
+計算機科学における抽象化って何? 数学における抽象化とどうかかわっているの?(Colburn & Shute 2007; Fine | |
2008; Hale & Wright 2001) | |
+形式技法って何?何が形式的なの?形式技法と形式的でない技法はどうちがうの?(Bowen & Hinchey 2005; Bowen & | |
Hinchey 1995) | |
+計算機科学ってどんな分野なの? 数学的モデル化と実験の役割は何?(Minsky 1970; Denning 1980; Denning | |
1981; Denning et al. 1989; Denning 1985; Denning 1980b; Hartmanis | |
1994; Hartmanis1993; Hartmanis 1981; Colburn 2004; Eden 2007) | |
+プログラムは科学理論と見なされるべきなのか?(Rapaport 2005a) | |
+計算機科学では数学はどういう風に利用されているか? 数学的モデルは記述的に使われているのか、それとも規範的に使われているのか?(White | |
2004; Turner 2007) | |
+<a href='http://ja.wikipedia.org/wiki/%E3%83%81%E3%83%A3%E3%83%BC%E3%83%81%EF%BC%9D%E3%83%81%E3%83%A5%E3%83%BC%E3%83%AA%E3%83%B3%E3%82%B0%E3%81%AE%E3%83%86%E3%83%BC%E3%82%BC'>チャーチ=チューリングのテーゼ</a>は論理学と数学における実質的 | |
/ 機械的方法の数学的観念を表現しているのか? | |
このテーゼは、人間による計算を表現しているのか?物理的機械にも適用されるものなのか?(Copeland 2004; Copeland | |
2007; Hodges 2006) | |
+<a href='http://en.wikipedia.org/wiki/Computational_thinking'>computational | |
thinking</a>という概念は、哲学的吟味に耐えられるものか?(Wing 2006) | |
+プログラムの正当性と終了を推論するために適切な論理はどれか?(Hoare 1969; Feferman 1992) | |
またそこでの論理選択はプログラミング言語にどういう風に依存するのか? | |
+情報とは何か?(Floridi 2004; Floridi 2005) この概念によってここに書いてあるような疑問がクリアになるのか? | |
+どうしてこんなにたくさんのプログラミング言語とプログラミングのパラダイムがあるのか?(Krishnamurthi 2003) | |
+プログラミング言語(とパラダイム)は科学理論の本質を持つか? プログラミングのパラダイムシフトは何をもたらすのか?(Kuhn 1970) | |
+ソフトウェア・エンジニアリングが哲学的テーマを呼ぶことはあるか?(Eden 2007) | |
<div class="note">* 詳細はよくわからなかった。</div> | |
いくつかのものについては、以下でもう少し説明する。 | |
*2* 2. 存在と同一性 | |
-計算機科学の対象や概念をどうやってカテゴライズ・個別化していけばいいか? | |
-物理的なもの(ルーターとかグラフィックカードとか)もあるし、抽象的なものもある(文法とか)。 | |
-プログラムやデータのような中心概念の特徴付けが一番問題だ。 | |
-「プログラムの存在論的地位」からして、はっきりしない部分があるし、同一性の基準もよくわからん。 | |
2.1 プログラムの二重の本質 | |
-プログラムは、テキストのような見かけも持っているし、機械のプロセスのような見かけをとることもある。 | |
-プログラムは編集されるテキストでもある一方で、ディスクの中にあるプログラムはまったくちがう性質を持っている。 | |
--たとえばディスクの中のプログラムは物理的なマシン上で実行可能である。 | |
-不可識別者同一の法則に従えば、この2つの見かけは同じものではありえない。 | |
--この両者の関係はきちんと説明されねばならない。 | |
-プログラムの物理的側面は、テキスト的なプログラムを「実装(implement)」したものだと考えられるかもしれない。 | |
-しかし「実装」って何だかよくわからない。 | |
--高級言語のプログラム(ソースコード)をマシン語(オブジェクトコード)に変換したものを「実装」と呼ぶこともある。 | |
--でもハードウェア上でソースコードを実現することも「実装」と呼んだりする。 | |
-この「実装」という概念をもう少し分析していかなければならない。 | |
-テキスト的対象がマシン上のプロセスを引き起すと考えたらどうか? | |
--テキストが現実の因果を引き起すというのはありえないんじゃないか。 | |
-プログラムの同一性という問題から考えると、もう少しちがった側面が見えてくる。 | |
--2つのプログラムが同一であると言われるのはいつなのか? | |
--ソフトウェアの法的な同一性について決定しようとするとプログラムの同一性が問題になってくる。 | |
--しかし、この問題について考えるためには意味論と実装についてもう少し説明しなければならない。 | |
*2_2* 2.2 プログラムとアルゴリズム | |
-概念を明確にするために、アルゴリズムとプログラムを区別しておく必要がある。 | |
--アルゴリズムはしばしば数学的な概念と考えられている。 | |
--しかし、アルゴリズムは数学だけじゃなく計算機科学の問題でもあるし、哲学的にももっと注目されてよい。 | |
-理論計算機科学と数理論理学の世界でアルゴリズムの数学的研究がなされてきたが、「アルゴリズムの本質」や「アルゴリズムとプログラムのちがい」といった哲学的問題はこれまであまり考えられてこなかった。 | |
-プログラムがテキスト的対象であるのに対し、アルゴリズムはその抽象的数学的対応者であると考えることはできるだろうか? | |
--こういう風に考えるなら、存在論的プラトニズムの一形式を選ぶことになる。 | |
--その場合、アルゴリズムが存在論的な優先性を持っていて、プログラムはアルゴリズムに到達するための言語的手段だということになる。 | |
--この方向でいくと、このタイプのプラトニズムの長所と短所を両方受け継ぐことになる。 | |
-プラトニズムよりじゃない考え方をするなら、プログラムによって表現された「アイデア」をアルゴリズムが保持していると考えることもできる。 | |
--この場合、プログラムとちがってアルゴリズムにはコピーライトは適用されない*。 | |
-そういう風に考えるなら、「アルゴリズム」という概念より、「アイデア」という概念や、その関連概念である「抽象化」を分析する必要がでてくるだろう。 | |
<div class="note">* おそらく、アルゴリズムは著作物じゃなくて「アイデア」の側にあるものだから、ということでしょう。</div> | |
*2_3* 2.3 プログラムと仕様記述 | |
-もう1つ吟味が必要な区別がある。プログラムと仕様記述の区別だ。 | |
-仕様記述とは何で、プログラムと何がちがうのか? | |
--この問題は哲学の文献ではあまり扱われてこなかったが、仕様記述の本質は、計算機科学の概念的基礎付けにかかわる基本的トピックだ。 | |
-形式的仕様記述の文献でよく見られる見方は、 | |
--プログラムがマシンに対する詳細な命令を含むのに対し、(関数型)仕様記述にはインプットとアウトプットの関係しか書かれない | |
-というものだ。 | |
-「手続き的/記述的」という区別を使って、これをもう少し敷衍することができる。 | |
--プログラムは手続き的なものであり、仕様書に記述された目的をいかにして達成するかを記述するものだ。 | |
-手続き的プログラミングの場合なら、これは適切かもしれないが、つねに当てはまるとはかぎらない。 | |
-論理型・関数型・オブジェクト志向プログラミングの場合は、話はかわってくる。 | |
--この手の言語でのプログラムは「手続き」ではなく「定義」によって構成されている。 | |
-しかも関数型仕様記述以外の仕様記述もある。 | |
--関数型以外の仕様では、インプットとアウトプットの関係ではなく、プログラムに含まれるかもしれない命令の種類や設計に対する要求を書く。 | |
-仕様とプログラムのちがいは、実装の概念にあるという見方もある。 | |
--仕様はコンパイルしたり実行したりできない、と。 | |
-しかし、もしこれが「コンパイラがない」という意味だとしたら、区別のための概念上の基準というより、偶然的な基準になってしまう。 | |
--前の世代では仕様記述言語だったものが、次の世代のプログラミング言語になるなんてことはよくある。 | |
-今日の仕様記述言語はしばしば明日のプログラミング言語だ。 | |
-仕様記述言語には、原理的に実装が存在しないという見方もある。 | |
--理由はおそらく、仕様記述言語には、チューリング計算可能でない概念も含まれるからだ。 | |
--仕様記述言語の多くは、ZF集合論と高階の論理に基づいている。 | |
-しかし仕様記述言語の特徴が「計算不可能な性質と関係を表現できること」にあるというのは変だろう。 | |
-計算不可能な要求を実践で使うことなんてあるだろうか? | |
-以上のようにたくさんの見方があることからして、仕様記述とプログラムの区別はもっと注目されてよいPCS上のトピックである。 | |
--概念の明確化のためだけではなく、これは未来のプログラミング言語と仕様記述言語のデザインに示唆をもたらすだろうから、もっと注目されてよい。 | |
*3* 3. 意味論 | |
-プログラミング言語の文法によって、正しいシンタクスが決まる。 | |
-しかし文法だけでは意図された意味を知ることはできない。文法だけをもとにしてプログラムを書くわけではない。 | |
-意味論はプログラマーやコンパイラ制作者や理論家に情報を与える。 | |
-ここまでは、意味論の文献に書いてあるふつうの見方だが、いろいろな概念を明確にしていく必要がある。 | |
*3_1* 3.1 表示的意味論と操作的意味論 | |
-プログラミング言語の意味論で、もっとも重要な区別は、「操作的意味論」と「表示的意味論」の区別だ。 | |
-操作的意味論は、プログラミング言語を抽象マシン上の命令として解釈する。 | |
-表示的意味論は集合や圏のような数学的な構造に対する解釈を与える。 | |
-しかし、操作的意味論だって数学的構造を与えるし、表示的意味論を抽象マシン上の命令として解釈することもできる。 | |
-意味論の合成性に注目した区別もある。 | |
--複合的な表現の意味論的値が、その諸部分の意味論的値の関数であるなら、意味論は合成的であるとされる。 | |
--合成性はとても重要な基準だ。 | |
--なぜなら合成性に注目することで、複雑なプログラムをどういう風に理解し、どういう風に構築していくかを明らかにできるからだ。 | |
--しかし、合成性に注目しても「操作的意味論」と「表示的意味論」の区別には役立たない。 | |
-結局のところ表示的意味論と操作的意味論の区別はあんまりはっきりしたものではない。 | |
*3_2* 3.2 実装と意味論的解釈 | |
-マシン語にコンパイルする(実装)のと、意味論的解釈を与えるのはどうちがうのだろうか。 | |
-ラパポートによれば、「実装」という概念は、意味論的解釈として理解されるべきものらしい。 | |
-コンパイルされたコードは、ソースコードに対する意味論解釈に相当する*。 | |
<div class="note">* | |
コンパイルすることで、ソースコードに現実のマシン上の「動作」が割り当てられる。これって結局意味論的な解釈をほどこしているのと同じことだろう、ということじゃないかと思われる。</div> | |
-ここで「実装」をふつうの意味で理解するなら、物理的なマシンが意味論的なドメインを与えることになる。 | |
--たとえば、C++の意味論は、Bjarne*のコンパイラを動かすBjarneのコンピューターによって決定されるってことになる。 | |
<div class="note">* Bjarne StroustrupはC++の制作者。</div> | |
-しかしこの説明は十分ではない。 | |
-BjarneのマシンによってC++で書かれたプログラムの意味が決定するなら、誤解釈や機械の不調についてはどう考えればよいのだろう。 | |
--Bjarneのマシンがおかしな動作をすることだってあるだろう。 | |
-じゃあ「おかしな動作」をするというのはどういうことだろう。 | |
--「壊れたマシンは意図された意味を具体化していない」ってことじゃないか?* | |
-こういう風に考えるなら、結局マシンとは独立に「意味」を考えなければならない。 | |
--つまり「実装」に訴えても、意味論を定義できるわけではない。 | |
<div class="note">* 原文ではクリプキの『ウィトゲンシュタインのパラドックス』が参照されている。</div> | |
*3_3* 3.3 意味論、等価性、同一性 | |
-2.1で「プログラムの同一性、等価性の話は意味論を扱ってから」と言ったが、意味論的説明というのはどれもプログラムの等価性を決定するものだ。 | |
-2つのプログラムは、意味論的値が等しいとき、等価であるとされる。 | |
--たとえば表示的意味論であれば、等価なプログラムは同じ数学的関数を計算する。 | |
-たとえば次の2つのプログラムは等価なものと判断される。 | |
>| | |
function Factorial(n: integer): integer | |
begin | |
if n = 0 | |
then Factorial := 1; | |
else | |
Factorial := (n) * Factorial(n-1); | |
end; | |
|< | |
>| | |
function Factorial(n: integer): integer | |
var | |
x, y: integer; | |
begin | |
y := 1; | |
x := 0; | |
while x<n do begin | |
x := x+1; | |
y := y*x; | |
end; | |
Factorial := y; | |
end; | |
|< | |
-一方、より操作的な見方をすれば、計算のステップ数を考慮し、この2つは等価ではないと見なされる。 | |
-異なる意味論的説明は異なった等価性の概念を持っているし、異なった概念的・実践的目的を持っている。 | |
-同一者不可識別の原理は、標準的な述語論理に組み込まれている原理だ。 | |
--同一者不可識別の原理によれば、2つの対象が等価なら、両者はすべての性質を同じくする。 | |
-不可識別者同一の原理は、この逆である。 | |
--不可識別者同一の原理によれば、すべての性質を共有する2つの対象は等価である。 | |
--対偶を考えれば、2つの対象が異なるものであるなら、一方のみが持っている性質が少なくとも1つある。 | |
-「同一者不可識別」と「不可識別者同一」を合わせて「ライプニッツの法則」と言うこともある。 | |
-ライプニッツの法則はしばしば等価性という概念の本質であるとされる。 | |
-この同一性の基準は、(プログラムの場合)観測等価性(observational equivalence)という形でより具体化されている。 | |
-2つのプログラムMとNが観測等価である必要十分条件は、 | |
--すべてのコンテキストC[...]において、 | |
--C[M]が妥当なプログラムならば、C[N]も妥当なプログラムであり、同じ意味論的な値を持つことだ。 | |
-たとえば、2つのリレーショナルデータベースシステムが観測等価であると言えるための必要十分条件は、 | |
--操作に対する何らかの意味論的説明において | |
--「同じ」コンテキスト(OS、マシンアーキテクチャー、インプット...etc.)で | |
--同じデータベースをつくりだすことである。 | |
-もちろんすべてのコンテキストでプログラムのふるまいを観測できるわけではない。しかし観測等価性は、不可識別者同一の原理から生じた潜在するコンセプチュアルな要求を反映しているはず。 | |
-観測的に区別されるすべてのプログラムが異なる意味論的値を持つなら、意味論は<em>健全</em>であると言われる。 | |
--つまり、意味論的に等価ならば、観測的にも区別されない。 | |
--同一者の不可識別性 | |
-異なる意味論的値を持つプログラムが観測的に区別されるなら、意味論は<em>完全</em>であると言われる。 | |
--つまり、観測的に区別されないならば、意味論的に等価である。 | |
--不可識別者の同一性 | |
-健全であり、かつ完全である意味論は、<em>full abstract</em>と言われる。 | |
--つまり、full abstractな意味論はライプニッツの法則を満たす。 | |
-意味論の論理学的バックグラウンドは、哲学的にも意味論の選択基準になる。 | |
--表示的意味論の多くは、full abstractではない。 | |
--最近の意味論では、表示的な意味論を与えるfull abstractな意味論的定義の研究が中心的トピックになっている。 | |
-意味論は計算機科学にとって、規範的な役割を果すものだ。 | |
--意味論がなければシンタクティカルな記述には内容が与えられず、実践的目的にも哲学的目的にも役立たない。 | |
*4* 4. 証明とプログラム | |
-仕様記述は「正当性」の概念にかかわる。 | |
-プログラムが仕様記述によって決められたインプットとアウトプットの関係を満たすとき、プログラムは(関数型)仕様記述に関し正当であるとされる。 | |
-より正確には、<i>p</i>をあるプログラムとし、それが仕様記述<i>R</i>満たすとする。 | |
--仕様記述は、インプット型<i>I</i>とアウトプット型<i>O</i>の関係とされる。 | |
-このとき | |
>>| | |
すべてのインプットに対し、型<i><b>I</b></i>の<i>i</i>および対<i>(i, | |
p(i))</i>が、関係<i><b>R</b></i>を満たす | |
|<< | |
-ここで、<i>p(i)</i>は、インプット<i>i</i>に対し、プログラム<i>p</i>を走らせた結果である。 | |
-関係<i>R</i>は何らかの仕様記述言語で書かれる。 | |
--仕様記述言語は多くの場合述語論理のバリアントであり、正当性の証明は論理の証明系によって実行される。 | |
--ホーア論理がよく使われる。 | |
-正当性の問題にかかわる哲学的議論のなかには、この証明の本質を問題にしたものもある。 | |
*4_1* 4.1. コンピュータサイエンスにおける証明 | |
-プログラムの正当性の証明は、本当の数学的証明なのだろうか? | |
-DeMillo et al. (1979)は、正当性の証明は冗長で数学的に浅薄なので、数学における証明とは違うと主張した。 | |
-その手の証明は、プログラム自体よりとても長い。 | |
-しかも、ホーア論理での推論は、ふつう暗黙のままにしておかれるような細部を必要とする。 | |
-この議論は、数学の哲学における「議論の把握可能性」と並行している(e.g., Tymoczko 1979; Burge 1988)。 | |
-核心にあるのは認識論的な問題である。 | |
--あまりに長く扱いにくく退屈な証明は、通常の数学の証明が持っているような確実性の担い手になることができない。 | |
-正当性の証明から得られる知識は、数学の証明から得られる知識とは異なっていると主張される。 | |
-ある観点からすれば、証明が正しいか間違っているかは認識論的な判断から独立である。 | |
-しかしここで問題になっているのは本質的に社会学的な観点なので、この両者の区別はつけておいた方がいい。 | |
--より実在論的な立場に立って、「証明は把握される必要がある」などという考えは捨てて、証明は正しいか間違っているかどちらかであると考えることもできる。 | |
-もっと強い立場に立って、正当性の証明は人間よりコンピューターがすべきであると考えることもできるだろう。 | |
--しかしもちろん証明チェッカー自体もチェックされなければならない。 | |
*4_2* 4.2 数学における証明 | |
-数学的証明も長くて複雑である。 | |
--しかし、そうした証明が数学者の共同体にとって理解可能になるのは、モジュール化の技法(定理など)や抽象化のおかげである。 | |
-新しい概念を導入することで、証明は少しずつ構成され、より理解しやすくなる。 | |
-数学的概念の発明によって、より高次の、より一般的な証明を構成できる。 | |
--たとえば指数表記のおかげで、乗法よりも複雑な計算を実行できるし、その結果を議論することもできる。 | |
-極端な例をあげれば、圏論ができたおかげで、代数的構造についての非常に一般的な結果について、主張したり証明したりしやすくなった。 | |
-数学は証明をするだけではない。数学には、抽象化や、新しい概念や表記法の創造も含まれるのである。 | |
-正当性の形式的証明には、概念の創造や抽象化のプロセスが含まれていない。 | |
-計算機科学では「抽象化」はプログラムのデザインに集中している。 | |
--数学における抽象化と計算機科学における抽象化については、あとでまた触れる。 | |
*4_3* 4.3 | |
-認識論的な心配以外にも、正当性の証明に対する批判はある。 | |
-正当性の証明によって保証されるのは、プログラムのテキスト的表現の正当性だけに思える。 | |
-物理的なマシンの上で実行したとき、期待された通りに動く保証はない(Fetzer 1988; Fetzer 1999; Colburn 2004)。 | |
-しかしプログラムが正当であるというのはどういうことだろう? | |
-あるプログラムが仕様を満たすためのテストを通過したとする。 | |
-これによって<em>テキスト的</em>プログラムの<em>物理的</em>対応者が実際に正当であるという経験的証拠が得られるはずだ。 | |
-この観点からすれば、テストされているのは、テキスト的プログラムではなく物理的対応者の側である。 | |
-以上の分析によれば、プログラムの正当性という概念には二重性があることになる。 | |
-プログラムの二重の本質に基づき、 | |
--テキスト的プログラムは数学的正当性に属し、 | |
--物理的対応者は経験的検証に属する | |
-と言えるかもしれない。 | |
*5* 計算可能性 | |
-計算可能性は計算機科学の哲学の最も古いテーマだ。 | |
-しかし<a href="http://plato.stanford.edu/entries/computability/">計算可能性の項はいくつか別にある</a>ので、2、3のトピックに触れるだけにする。 | |
--<a href='http://plato.stanford.edu/entries/computability/'>Computability | |
and Complexity (Stanford Encyclopedia of Philosophy)</a> | |
--<a href='http://plato.stanford.edu/entries/church-turing/'>The | |
Church-Turing Thesis (Stanford Encyclopedia of Philosophy)</a> | |
--<a href='http://plato.stanford.edu/entries/turing-machine/'>Turing | |
Machines (Stanford Encyclopedia of Philosophy)</a> | |
**5_1* 5.1 チャーチ-チューリングのテーゼ | |
-主要なトピックの1つはチャーチ-チューリングのテーゼだ。 | |
-議論はこのテーゼの2つの解釈にかかわっている。 | |
-I. チューリングマシンは「一般的原則[rule of thumb]」や「純粋に機械的」と言われるようなことは何でもできる。 | |
-II. マシンによって計算できること(有限な命令からなるプログラムと有限なデータできること)は何でもチューリングマシン計算可能である。 | |
-Iの解釈は論理学や数学における「実効的」「機械的」方法の概念を捕捉している。 | |
-数学において暗黙的に使用されたりヒルベルトのプログラムで明らかになったアルゴリズムの非形式的な概念を反映している。 | |
-IIの方は物理的なマシンを対象にしている。 | |
-(Gandy 1980)はIIの方の解釈を展開している。 | |
-Gandyは物理的なマシンの計算を特徴づける4つの原理を提案し、それがチューリングの定式化と一致することを示した。 | |
--ただし表示的意味論で考えられるようなマシンはGandyのマシンより高度のな動作をするし、この原理を満さない。 | |
-チャーチとチューリングはIの意味で考えていて、マシンに制約を設定していないという人もいる(Copeland 2004; Copeland 2008)。 | |
-チャーチとチューリングは2つの解釈を区別していないという人もいる(Hodges 2007)。 | |
-↑こういう歴史的議論とは別に物理的な議論もなされていて、そっちは現実のマシンの能力にかかわっている(解釈II)。 | |
-現存する実装のあるプログラミング言語で書かれたプログラムはチューリング可能 | |
-プログラミング言語の目的はチューリング完全であり、万能チューリングマシンをシミュレートできるだけの構造を持っている。 | |
-Copeland (2007)は、Gandyの定式化は狭すぎると主張している。 | |
-将来的にはチューリング計算可能な関数の範囲を越える物理的マシンもできるかもしれない。 | |
-そのためには無限のスピードアップが必要であり、それによって無限の計算を有限時間内に実行できる。 | |
-量子計算はそうしたマシンの例としてあげられたが、これは論破された。 | |
-Hodgesは物理学における標準的な数学的議論の応用可能性について述べている。 | |
-そうした応用には無限の正確さが必要になったりするのだ。 | |
-というわけで、これは単に経験的な問題というわけではない。 | |
-Dummett (2006)は無限のタスクが物理的な領域の中で実行されるというのは物理的に不可能なばかりではなく、概念的にも不可能ではないかと疑問視している。 | |
-つまりこの議論は、経験的な問題というだけではなく、数学的モデルと物理的なリアリティの関係についてのわれわれの理解の核心に踏みこもうとしているのである。 | |
*6* 6. プログラミングとプログラミング言語 | |
-抽象化はコンピュータサイエンスの概念的な基礎だ。 | |
-プログラミングのデザインや構造の欠かせない一部であるし、プログラミング言語のデザインのコアな方法論でもある。 | |
-以下の概念の創造には抽象化が関わっている。 | |
--手続き型および関数型抽象化、ポリモーフィズム、データ抽象、オブジェクトとクラス、デザインパターン、アーキテクチャスタイル、サブタイピングと継承 | |
-ソフトウェアエンジニアリングにも抽象化は欠かせない。 | |
-コンピュータサイエンスにおける抽象化の本質は何だろう? | |
-抽象化という概念自体、哲学的に問題がある。 | |
-伝統的な見方によれば、抽象化は哲学的心理学に由来し、「複数の対象や観念から特徴を省略しつつ考慮することによって新しい概念をつくるような心理的プロセス」のことである(Rosen | |
2001)。 | |
-今このアプローチを採用することに哲学的アドバンテージはほとんどない。 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment