アドホック多相(1)／パラメトリック多相(2)

[0001 考える名無しさん 2022/06/19(日) 09:59:59.04 0]

1.単一の名前が、複数の異なる関数を指している
2.単一の名前が指す（単一の）関数が、複数の異なる型で使用できる

指示とは、哲学である

[0002 考える名無しさん 2022/06/19(日) 10:01:17.45 0]

[名指しと必然性]はクリプキの代表的な著作である

クリプキは1970年からプリンストン大学にて指示理論に関する
指示の因果説を提唱する講義を行った。この著作は1970年の
講義の内容をまとめたものである。固有名はどのように
世界の事物を指示すのか、同一性の本質とは何かという
分析哲学の問題に関する研究業績である

1960年代まではラッセルが提唱してフレーゲにより発展された
記述理論の研究により、固有名と確定記述を同義として見なしていた
この著作でのクリプキの研究の目的とはそのような見方に対する批判である

クリプキはXとYが同一であるならばXがYであることは必然であると考えて
同一性の必然性を出発点とした。そして固有名と確定記述が同義ではない
ことを考察する

[0003 考える名無しさん 2022/06/19(日) 10:01:45.74 0]

アリストテレスという固有名を考えてみると、同一性の必然性から
アリストテレスはアレキサンダー大王の教師であるという確定記述は
真であるとは限らないが、アリストテレスがアリストテレスであることは
必然的に真である。したがって、アリストテレスという固有名と
アリストテレスがアレキサンダー大王の教師であるという確定記述は
同義ではありえない。

なぜならば、アリストテレスという固有名には固定指示子(rigid designator)がある一方で、
確定記述はアレクサンドロス大王の教師であったアリストテレスではない人物を指示することが
可能であるためである。

この固有名と確定記述の関係は自然科学の命題にもあてはまり、例えば金という
固有名と原子番号79番の元素という確定記述とは、前者の固定性が権利上のものであるが、
後者の固定性が事実上のものであるために同義ではないと指摘される

[0004 考える名無しさん 2022/06/19(日) 10:25:41.56 0]

パラメトリック多相関数は自然変換になるが、アドホック多相関数は「自然変換」にならない、と
思っている人がいるかも知れないが、そんなことはない。アドホック多相関数でも
「自然変換」に仕立てることができる

[0005 考える名無しさん 2022/06/19(日) 10:44:55.56 0]

たとえば、「このはし渡るべからず」という立て札による禁止を指す指示物は、
一休さんによって多相化されて、ハシでなく、真ん中を歩いていけば良い、と
いう内容に変換される

一休さんにとっては、これが「自然変換」になる

[0006 考える名無しさん 2022/06/19(日) 10:52:48.27 0]

人間を関数である程度定義できるとすれば、そこから様々な関数を
パラメトリック多相関数として定義できるかもしれない

第一の関数にしたいのは、「人間は、ホモサピエンスである」
になる

つまり、人間は猿と同じようなものであってはならないというもの
愚行権という概念もあるが、それはホモサピエンスがあっての、
そこから逸脱した派生物になる

[0007 考える名無しさん 2022/06/19(日) 11:08:21.57 0]

ポリモーフィズム（polymorphism）とは、それぞれ異なる型に一元アクセスできる
共通接点の提供、またはそれぞれ異なる型の多重定義を一括表現できる
共通記号の提供を目的にした、型理論またはプログラミング言語理論の概念および実装である

この用語は、有機組織および生物の種は様々な形態と段階を持つという生物学からの
借用語である。多態性、多相性と邦訳されることが多い

[0008 考える名無しさん 2022/06/19(日) 11:09:26.47 0]

ポリモーフィズムは、通常以下の三種に分けられる

アドホック多相（ad hoc polymorphism）- 恣意的な型の集合に一つの共通接点を提供する
関数オーバーロード、Mix-inの一実装、型クラスなど

パラメトリック多相（parametric polymorphism）- 詳細化されていない型要素を
内包する抽象的な型に記号表現を提供する。ジェネリクスや関数型言語の型構築子など

サブタイピング（subtyping）- サブタイプ多相（subtype polymorphism）や
インクルージョン多相（inclusion polymorphism）とも。
上位型をその下位型の数々で代替できるようにする。オブジェクト指向の多態性はこれを指す

この他に、ロー多相（row polymorphism）とポリタイピズム（polytypism)も挙げられることがある。
対義語はモノモーフィズム（Monomorphism）である

[0009 考える名無しさん 2022/06/24(金) 19:13:17.82 0]

同じ引数が、常に同じ結果を生成するというルールを
プログラミング言語の関数に適用することを「参照透過性」と呼ぶ

[0010 考える名無しさん 2022/06/24(金) 19:33:55.50 0]

ラムダ計算はチューリングマシーンに匹敵する普遍的な計算モデルを
可能にした。ラムダ計算は1930年代に数学者のアロンゾ・チャーチ
関数と変数(x,y)のみを使用する論理システムを作成したが、この
論理システムのことをラムダ計算と呼ぶ

ラムダ計算では、すべてのものが関数として表される
たとえば、真と偽は関数であり、すべての整数も関数として表せる

[0011 考える名無しさん 2022/06/24(金) 19:48:18.79 0]

チャーチ＝チューリングのテーゼ (Church-Turing thesis) もしくはチャーチのテーゼ
(Church's thesis) とは、「計算できる関数」という直観的な概念を、帰納的関数と呼ばれる
数論的関数のクラスと同一視しようという主張である。テーゼの代わりに提唱や定立の語が
用いられることもある。このクラスはチューリングマシンで実行できるプログラムのクラス、
ラムダ記法で定義できる関数のクラスとも一致する。よって簡単にはテーゼは、計算が
可能な関数とは、その計算を実行できるような有限のアルゴリズムが存在するような関数、
よっておおよそコンピュータで実行できる関数と同じだと主張する

[0012 考える名無しさん 2022/06/24(金) 19:49:05.66 0]

1932年にエルブラン、および1934年にゲーデルが、原始帰納的関数と呼ばれる自然数上の
関数の明示的構成法を拡張して帰納的関数（もしくは一般帰納的関数）と呼ばれる
関数の構成法を作り上げた。1933年から1935年ごろには、チャーチやクリーネが
やはり関数の構成的な定義法であるラムダ記法を用いて定義可能な関数のクラスを定めた。

さらに、1935年から1936年にかけてポストとチューリングは、チューリングマシンの概念を
用いてこの理念的計算機械で実行可能なプログラムのクラスを定めた

[0013 考える名無しさん 2022/06/24(金) 19:50:00.45 0]

こうしてほぼ同時期に出現したさまざまな計算できる数論的関数のクラスは、実は互いに
同じものであることが証明された。これにより、それまで非形式的に「実質的に計算できる関数」
(effectively computable function) と呼び慣わされていたこのクラスをもってして
「計算できる関数」とみなそうという主張がなされることになった。

これがチャーチ＝チューリングのテーゼと呼ばれている主張である。この意味で計算できる関数は
チューリング計算可能な関数、あるいは単に計算可能関数と呼ばれるようになった

[0014 考える名無しさん 2022/06/24(金) 20:16:43.35 0]

スレチ

[0015 考える名無しさん 2022/06/24(金) 20:37:39.27 0]

REPL 【Read-Eval-Print Loop】

REPLとは、プログラミング言語の実行環境の一つで、利用者が入力欄に
キーボードなどから式や文を一行入力すると、即座に解釈・実行して結果を返し、
再び入力可能になるもの。インタプリタの一種。

[0016 考える名無しさん 2022/06/25(土) 10:31:02.55 0]

モンタギュー文法

モンタギュー文法は、自然言語の意味論へのアプローチの一つ。アメリカ合衆国の論理学者
リチャード・モンタギューの名を採って名付けられた

モンタギュー文法は形式論理学、特にラムダ計算と集合論にもとづき、内包論理とタイプ理論も
利用している。モンタギューはこのアプローチを1960年代から1970年代の初頭にかけて率先した。

モンタギューによれば（英語のような）自然言語の意味論と（述語論理のような）形式言語の
それとの間に本質的な違いはない。モンタギュー文法の中心的な概念は論文
"The Proper Treatment of Quantification in Ordinary English" ではじめて提案された。

モンタギューの量化の扱いはプログラミング意味論の継続の概念と関連付けられている

[0017 考える名無しさん 2023/08/11(金) 18:55:42.69 0]

よく頑張ったね