Wikipedia

「利用者:I.hidekazu/直観主義型理論」の版間の差分

履歴の双方向閲覧
← 古い編集新しい編集 →
削除された内容 追加された内容
ビジュアルウィキテキスト
編集の要約なし
編集の要約なし
10行目:
直観主義型理論の型構築子（type constructor）は、論理演算子（logical connective）と一対一で対応するように作られている。例えば、含意と呼ばれる論理演算子（<math>A \implies B</math>）は、関数型（<math>A \to B</math>）に対応する。この対応は[[カリー＝ハワード同型対応]]と呼ばれる。かつての型理論もこの同型対応に従っていたが、現在のマルティン＝レーフの型理論は[[依存型]]（dependent type）を導入することによって述語論理をそのように拡張した最初のものである。
 
==Type theory型理論 ==
直観主義型理論は３つの有限型を持つ。その有限型は５つの異なる型構築子（type constructor）を組み合わせたものである。集合論とは異なり、型理論は第一階述語論理のような論理学をベースに構築されてはいない。だから、それぞれの型理論の特徴は、数学と論理学両方の特徴としての役割を果たす。
Intuitionistic type theory has 3 finite types, which are then composed using 5 different type constructors. Unlike set theories, type theories are not built on top of a logic like [[First-order logic|Frege's]]. So, each feature of the type theory does double duty as a feature of both math and logic.
 
''型理論に親しんでいないが、集合論を知っているという人に対する簡単な要約は次のとおりである。集合が元を含むのと同じように型は項（term）を含む。項は一つそしてただ一つだけの型に属する。<math>2+2</math> や <math>2\cdot 2</math>のような項は計算（簡約）すると4のようなカノニカルな項（canonical term）になる。さらに知りたい場合は[[型理論]]の記事を参照せよ''
''If you are unfamiliar with type theory and know set theory, a quick summary is: Types contain terms just like sets contain elements. Terms belong to one and only one type. Terms like <math>2+2</math> and <math>2\cdot 2</math> compute ("reduce") down to canonical terms like 4. For more, see the article on [[Type theory]].''
 
===0 type, 1 type and 2 type ===
「https://ja.wikipedia.org/wiki/利用者:I.hidekazu/直観主義型理論」から取得