[過去ログ]
現代数学の系譜 工学物理雑談 古典ガロア理論も読む71 (1002レス)
現代数学の系譜 工学物理雑談 古典ガロア理論も読む71 http://rio2016.5ch.net/test/read.cgi/math/1561208978/
上
下
前次
1-
新
通常表示
512バイト分割
レス栞
抽出解除
レス栞
このスレッドは過去ログ倉庫に格納されています。
次スレ検索
歴削→次スレ
栞削→次スレ
過去ログメニュー
217: 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE [sage] 2019/06/24(月) 17:00:59.73 ID:dnjTnHb1 >>216 つづき https://ja.wikipedia.org/wiki/%E3%82%B3%E3%83%B3%E3%83%93%E3%83%8D%E3%83%BC%E3%82%BF%E8%AB%96%E7%90%86 コンビネータ論理(Combinatory Logic、組み合わせ論理)は、モイセイ・シェインフィンケリ(ロシア語版、英語版): Moses Ilyich Schonfinkel)とハスケル・カリー(英: Haskell Brooks Curry)によって、記号論理での変数[要曖昧さ回避]を消去するために導入された記法である。 最近では、計算機科学において計算の理論的モデルで利用されてきている。また、関数型プログラミング言語の理論(意味論など)や実装にも応用がある。 コンビネータ論理は、コンビネータまたは引数のみからなる関数適用によって結果が定義されている高階関数、コンビネータに基づいている。 数学におけるコンビネータ論理 コンビネータ論理は元来、本質的に量化変数を消去することによって量化変数の役割を明確にするような「pre-logic」を意図していた。量化変数を消去する方法にはクワインの述語関手論理がある。コンビネータ論理の表現力は一階述語論理を超える一方、述語関手論理の表現力は一階述語論理と同等である。 1927年後半、カリーはプリンストン大学の講師として働いているときにコンビネータを再発見した。[1]1930年代後半、アロンゾ・チャーチとプリンストン大学の彼の教え子が、ラムダ計算というライバルとなる関数抽象の形式化を考案し、コンビネータ論理より人気を博すこととなった。 こうした歴史的偶然のために、理論計算機科学が60?70年代にコンビネータ論理に関心を持ち始めるまで、この分野のほとんどすべての業績は、ほとんどカリーとその教え子、もしくはベルギーのロベール・フェイ(英語版)によるものであった。Curry and Feys (1958) および Curry et al. (1972) はコンビネータ論理の初期の歴史についてのサーベイ論文である。 より最近のコンビネータ論理とラムダ計算の比較については Barendregt(オランダ語版、英語版) (1984) を参照されたい(デイナ・スコットが60?70年代に考案したコンビネータ論理のためのモデル理論についても触れている)。 (引用終わり) 以上 http://rio2016.5ch.net/test/read.cgi/math/1561208978/217
218: 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE [sage] 2019/06/24(月) 17:10:21.30 ID:dnjTnHb1 >>217 補足 圏論とも関連していたような(^^ https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C カリー=ハワード同型対応 通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種と関係している。[要出典] (抜粋) 目次 1 一般的な定式化 2 ヒルベルト流の推論体系とコンビネータ論理との間の対応 3 自然演繹とラムダ計算との間の対応 4 古典論理と制御演算子との間の対応 5 シークエント計算 6 再帰型と自己言及 7 「証明=プログラム」対応に関連する話題 7.1 ド・ブランの役割 7.2 BHK解釈 7.3 実現可能性解釈 7.4 カリー=ハワード=ランベック対応 8 例 8.1 恒等コンビネータと α → α のヒルベルト流の証明 8.2 合成コンビネータと (β → α) → (γ → β) → γ → α のヒルベルト流の証明 8.3 (β → α) → (γ → β) → γ → α の自然演繹における証明とラムダ項 9 その他の応用 カリー=ハワード=ランベック対応 ヨアヒム・ランベックは1970年始めに直観主義命題論理とデカルト閉圏の等式理論と対応するある種の型付きコンビネータとの対応関係の証明を示した。 このカリー=ハワード=ランベック対応は直観主義論理、型付きラムダ計算およびデカルト閉圏との間の対応として知られる。 http://rio2016.5ch.net/test/read.cgi/math/1561208978/218
メモ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
スレ情報
赤レス抽出
画像レス抽出
歴の未読スレ
AAサムネイル
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.031s