ブラウザよりも高速アクセス！
33 関係: 型付きラムダ計算、型システム、型推論、多重集合、変数 (数学)、対称関係、導出原理、帰納的可算集合、一階述語論理、交換法則、アリティ、ジョセフ・ゴーグエン、等式、省略、結びと交わり、結合法則、組合せ爆発、順序集合、項書き換え、計算言語学、計算機科学、論理プログラミング、論理積、自動推論、Haskell、Prolog、推移関係、恒等式、恒真式、束 (束論)、束縛 (情報工学)、決定可能性、数理論理学。
型付きラムダ計算
型付きラムダ計算（typed lambda calculus）とは、無名の関数の抽象表現にラムダ (\lambda) というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。 ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。 様々な型付きラムダ計算がこれまで研究されてきた。単純型付きラムダ計算はいくつかの基本型（または型変数）と関数型 \sigma\to\tau から成る。System T はこれを拡張し、自然数型と高階原始再帰を加えたものである。この系ではペアノ算術において全ての再帰する可能性のある関数が定義可能である。System F は、全ての型に対して全称量化を施すことでポリモーフィズムを実現している。これを論理学的に見れば、二階述語論理に属する全ての関数を記述できることを意味する。依存型のあるラムダ計算は直観主義的型理論の基盤であり、calculus of constructions や logical framework (LF) の基盤である。Berardi の成果に基づき Barendregt が提案したラムダ・キューブは、純粋な型付きラムダ計算（単純型付きラムダ計算、System F、LF、calculus of constructions など）の関係を体系化したものである。 一部の型付きラムダ計算には「派生型」の記法が導入されている。すなわち、A が B の派生型であるとき、型が A である全ての項は型が B でもある。派生型のある型付きラムダ計算は単に普通の型付きラムダ計算に結合型 (conjunctive type) と F^\leq (F-sub) を加えたものである。 以上の体系はすべて（型のないラムダ計算以外）、「強く正規化 (strongly normalizing)」する。すなわち、全ての計算は停止する。結果としてそれらは論理として一貫しており、uninhabited types がある。しかし、強く正規化しない型付きラムダ計算も存在する。全ての型の型 (Type: Type) を持つ依存型付きラムダ計算は Girard's paradox により正規化しない。この系は最も単純な純粋型システムでもあり、ラムダ・キューブを一般化した形式手法である。明示的な再帰コンビネータを持つ系（Gordon Plotkin の PCF など）も正規化しないが、論理体系として解釈されることを意図していない。実際、PCF (Programming language for Computable Functions) は型付き関数型プログラミング言語であり、型はプログラムが正しく動作することを保証する目的で使われているが、必ずしも停止を保証しない。 型付きラムダ計算はプログラミング言語の新たな型システムの設計で重要な役割を演じている。型付け可能性は一般にプログラミングの好ましい属性を捉え、例えば、プログラムがメモリアクセス違反を起こさないようにするといったことが考えられる。 プログラミングにおいて、強い型付けのプログラミング言語のルーチン（関数、プロシージャ、メソッド）は、型付きラムダ計算と密接に関連している。Eiffelには "inline agent" の記法があり、型付きラムダ式を直接定義して操作できる。例えば、agent (p: PERSON): STRING do Result.
新しい！!: ユニフィケーションと型付きラムダ計算 · 続きを見る »
型システム
型システム（type system）とは、プログラミング言語において、その式などの部分が持つ値を、その種類（型(type)、データ型も参照）に沿って分類し、プログラムが正しく振る舞うこと、といった性質について保証する手法である。型システムは、型理論に基づいており、プログラミング言語の理論において最も確立された軽量形式手法である。.
新しい！!: ユニフィケーションと型システム · 続きを見る »
型推論
型推論（かたすいろん）とはプログラミング言語の機能の1つで、静的な型付けを持つ言語において、変数や関数の型を宣言しなくてもそれを導くのに使われた関数の型シグネチャなどから自動的に型を決定する機構のこと。 推論に失敗するとその時点でエラーを報告できるため、少なくとも誤った型を用いる事によるバグは回避できる。また、記述をアルゴリズムに集中できるのでプログラムの抽象度が上がるというメリットもある。 代表的な型推論アルゴリズムとして、Hindley/Milner 型推論アルゴリズムがある。各々著名なコンピュータ科学者の名前からつけられた名前であるが、Hindley は論理学者として型推論システムを先に開発した。 型推論を持つ言語としてはHaskell、ML、Vala、F#、C#、Java、Scala、OCaml、D言語、Concurrent Clean、C++11、Swiftなどがある。静的型付け関数型言語のほとんどがなんらかの型推論の機能を持っている。.
新しい！!: ユニフィケーションと型推論 · 続きを見る »
多重集合
数学における多重集合（たじゅうしゅうごう、multiset）あるいはバッグ（bag; かばん）は、集合に同じ値の元がいくつも含まれるとき、各元がそれぞれいくつ含まれるかという重複度を考え合わせた集合概念である。非順序対、非順序組 (unordered tuple) ともいう。 クヌースによれば、1970年代に最初に多重集合 (multiset) という言葉を提案したのは、オランダ人数学者のニコラース・ホーバート・ド・ブラン (IPA) であるという クヌースは同書で、多重集合に対して提案された他の名前（例えば,リスト(list)、まとまり(bunch)、バッグ(bag)、堆積(heap)、標本(sample)、重みつき集合(weighted set)、コレクション(collection)、組(suite).など）も提示している。 多重集合の歴史に関するサーベイ論文である。 。しかし、数学における多重集合の概念は、"multiset" という名称がつけられる90年以上も前にすでに使用が認められる。実際、1888年に発表されたリヒャルト・デデキントの有名な論文 "Was sind und was sollen die Zahlen?" （「数とは何か、何であるべきか？」）において、実質的に多重集合の概念が用いられている。.
新しい！!: ユニフィケーションと多重集合 · 続きを見る »
変数 (数学)
数学、特に解析学において変数（へんすう、variable）とは、未知あるいは不定の数・対象を表す文字記号のことである。代数学の文脈では不定元（ふていげん、indeterminate）の意味で変数と言うことがしばしばある。方程式において、特別な値をとることがあらかじめ期待されている場合、（みちすう）とも呼ばれる。また、記号論理学などでは（変数の表す対象が「数」に限らないという意味合いを込めて）変項（へんこう）とも言う。.
新しい！!: ユニフィケーションと変数 (数学) · 続きを見る »
対称関係
対称関係（たいしょうかんけい、Symmetric relation）は、数学における二項関係の一種。集合 X における二項関係 R が「対称」であるとは、X に属する全ての a および b について、aRb が成り立つなら bRa も成り立つことをいう。 数学的に記述すると次のようになる。 対称関係と反対称関係（aRb かつ bRa ならば b.
新しい！!: ユニフィケーションと対称関係 · 続きを見る »
導出原理
導出原理（どうしゅつげんり、resolution principle）とは、により1965年に提案されたJ.
新しい！!: ユニフィケーションと導出原理 · 続きを見る »
帰納的可算集合
帰納的可算集合（きのうてきかさんしゅうごう、Recursively enumerable set）は、計算理論または再帰理論におけるある種の集合に付与された名前。自然数の集合 S について以下が成り立つ場合、その集合を指して帰納的可算、計算可枚挙、半決定可能、証明可能、チューリング-認識可能などと称する。.
新しい！!: ユニフィケーションと帰納的可算集合 · 続きを見る »
一階述語論理
一階述語論理（いっかいじゅつごろんり、first-order predicate logic）とは、個体の量化のみを許す述語論理 (predicate logic) である。述語論理とは、数理論理学における論理の数学的モデルの一つであり、命題論理を拡張したものである。個体の量化に加えて述語や関数の量化を許す述語論理を二階述語論理（にかいじゅつごろんり、second-order predicate logic）と呼ぶ。それにさらなる一般化を加えた述語論理を高階述語論理（こうかいじゅつごろんり、higher-order predicate logic）という。本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細は「二階述語論理」「高階述語論理」を参照。.
新しい！!: ユニフィケーションと一階述語論理 · 続きを見る »
交換法則
交換法則（こうかんほうそく、Commutative property) は数学における法則の一つ。可換則（かかんそく）や交換律（こうかんりつ）ともいう。.
新しい！!: ユニフィケーションと交換法則 · 続きを見る »
アリティ
アリティ (arity) とは、代数学、論理学、計算機科学などにおいて、関数や算法(演算) が取る引数（オペランド）の個数を意味する用語である。 項数のような訳語が当てられる場合もあるが、arityと英単語のまま用いられることも多い。 複合語としてならば、「変数」（例えば二変数函数、多変数函数）や単に「項」（二項演算、多項関係など）あるいはまた（不定元の数という意味で）「(-)元」（例えば二元連立一次方程式）などはアリティに言及する訳語として存外よく用いられるものである。（しかし同じ語でも、例えば数列や多項式などに用いられる「項」や「項数」はアリティではなく "term" に関する言及である。）.
新しい！!: ユニフィケーションとアリティ · 続きを見る »
ジョセフ・ゴーグエン
ョセフ・アマディ・ゴーグエン（Joseph Amadee Goguen、1941年6月28日 - 2006年7月3日）は、アメリカ合衆国の計算機科学者。.
新しい！!: ユニフィケーションとジョセフ・ゴーグエン · 続きを見る »
等式
等式（とうしき、equation）とは、二つの対象の等価性・相等関係 (equality) を表す数式のことである。.
新しい！!: ユニフィケーションと等式 · 続きを見る »
省略
省略（しょうりゃく、ellipsis、ギリシャ語：έλλειψις, élleipsis）とは、文中のある要素が欠如しているが、文脈から、あるいは論理もしくは全文のパターンから、それが何かを推断かつ復旧することが可能な修辞技法のこと。省略法を用いて作られた構文を省略構文（elliptical construction）という。.
新しい！!: ユニフィケーションと省略 · 続きを見る »
結びと交わり
半順序集合 において、部分集合 の結び (join) と交わり (meet) はそれぞれ の上限（最小上界） と の下限（最大下界） である。一般に、半順序集合の部分集合の結びや交わりは存在するとは限らない；存在するときには、それらは の元である。 結びと交わりは の元の対上の可換結合的冪等部分二項演算として定義することもできる。 と が の元であるとき、結びは と書かれ、交わりは と書かれる。 結びと交わりは順序の反転に関して対称である。全順序集合の部分集合の結び/交わりは単にその極大/極小元である。 すべての対が結びを持つような半順序集合は である。双対的に、すべての対が交わりを持つような半順序集合は である。join-semilattice でも meet-semilattice でもあるような半順序集合は束である。単にすべての対ではなくすべての部分集合が結びと交わりを持つような束は完備束である。すべての対が結びや交わりをもつわけではないがその演算が（定義されるときに）ある公理を満たすような を定義することもできる。.
新しい！!: ユニフィケーションと結びと交わり · 続きを見る »
結合法則
数学、殊に代数学における結合法則（けつごうほうそく、associative law) 、結合則、結合律あるいは演算の結合性（けつごうせい、associativity）は二項演算に対して考えられる性質の一つ。ひとつの数式にその演算の演算子が2個以上並んでいる時、その演算子について、左右どちらの側が優先されるかに関わらず結果が同じになるような演算は結合的 (associative) である。.
新しい！!: ユニフィケーションと結合法則 · 続きを見る »
組合せ爆発
組合せ爆発（くみあわせばくはつ、Combinatorial explosion）は、計算機科学、応用数学、情報工学、人工知能などの分野では、解が組合せ（combination）的な条件で定義される離散最適化問題で、問題の大きさn に対して解の数が指数関数や階乗などのオーダーで急激に大きくなってしまうために、有限時間で解あるいは最適解を発見することが困難になることをいう。.
新しい！!: ユニフィケーションと組合せ爆発 · 続きを見る »
順序集合
数学において順序集合（じゅんじょしゅうごう、ordered set）とは「順序」の概念が定義された集合の事で、「順序」とは大小、高低、長短等の序列に関わる概念を抽象化したものである。ただし、順序集合内の2つの元, に順序関係が定まっている（「比較可能」である）必要はなく、両者が「比較不能」であってもよい。 比較不能のケースを許容していることを強調して順序集合の事を半順序集合（はんじゅんじょしゅうごう、partially ordered set, poset）ともいう。一方、半順序集合の中で比較不能のケースがないものを特に全順序集合 という。（「半順序」という言葉が「全順序」の対義語ではない事に注意。全順序集合も半順序集合の一種である。） 全順序集合の簡単な例は整数の集合や実数の集合で、通常の大小比較を順序とみなしたものがある。 一方、全順序ではない半順序集合の例としては、正の整数全体の集合に整除関係で順序を入れたものや、（2つ以上元を含む）集合の冪集合において、包含関係を順序とみなしたものがある。例えば2元集合 において と はいずれも他方を包含していないので S の冪集合は全順序ではない。 実生活に近い例では、「AさんはBさんの子孫である」という事を「A＜B」という大小関係とみなす事で人間全体の集合を半順序集合とみなせる。AさんとBさんはどちらも他方の子孫でない事もありうる（兄弟同士、叔父と甥、赤の他人等）ので、この順序集合は全順序ではない。.
新しい！!: ユニフィケーションと順序集合 · 続きを見る »
項書き換え
項書き換え（こうかきかえ、term rewriting）とは、数学・計算機科学・論理学において、式（数式、論理式）の項を別の項に置換する手法を総称する用語である。項書き換え系（term rewriting system、TRS）とは、項の集合とその置換規則から構成される。 項書き換えは非決定論的になることがありうる。ある規則で書き換え可能な項が他の規則でも書き換え可能な場合がありえて、その場合は複数の規則が適用可能と言うことになる。項書き換え系では、項書き換えのためのアルゴリズムは提供されず、書き換え規則の集合のみが提供される。しかし、適当なアルゴリズムと組み合わせれば、項書き換え系はプログラムのような働きをし、実際いくつかの宣言型プログラミング言語は項書き換えに基づいている。.
新しい！!: ユニフィケーションと項書き換え · 続きを見る »
計算言語学
計算言語学（けいさんげんごがく、computational linguistics）とは、形式性を重視する言語学の一分野である。自然言語処理と共に「理科系言語学」と称される。 類似名称の言語学分野に計量言語学があるが、計量言語学は統計的な手法により自然言語を研究する分野であり計算言語学とは異なる。.
新しい！!: ユニフィケーションと計算言語学 · 続きを見る »
計算機科学
計算機科学（けいさんきかがく、computer science、コンピュータ科学）とは、情報と計算の理論的基礎、及びそのコンピュータ上への実装と応用に関する研究分野である。計算機科学には様々な下位領域がある。コンピュータグラフィックスのように特定の処理に集中する領域もあれば、計算理論のように数学的な理論に関する領域もある。またある領域は計算の実装を試みることに集中している。例えば、プログラミング言語理論は計算を記述する手法に関する学問領域であり、プログラミングは特定のプログラミング言語を使って問題を解決する領域である。.
新しい！!: ユニフィケーションと計算機科学 · 続きを見る »
論理プログラミング
論理プログラミング（Logic Programming）とは、広い意味では、コンピュータプログラミングでの数理論理学の使用である。この観点での論理プログラミングは、ジョン・マッカーシーのadvice takerの提案にまでさかのぼることができる。 より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。 論理をベースにしたプログラミング言語として1971年に Planner のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった。Plannerと独立してより論理を重視した Prolog が開発され、コワルスキーにより述語論理式(ホーン節)のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した。 Planner からの派生で、プログラミング言語 Poplerが開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、Oz、Fril などがある。バックトラッキングを使用しない並行論理プログラミング言語としてProlog からの派生したConcurrent Prolog、PARLOG、GHC、KL1などの各種言語（Shapiro に調査結果がある）がある。.
新しい！!: ユニフィケーションと論理プログラミング · 続きを見る »
論理積
数理論理学において論理積（ろんりせき、logical conjunction）とは、与えられた複数の命題のいずれもが例外なく真であることを示す論理演算である。合接（ごうせつ）、連言（れんげん、れんごん）とも呼び、ANDとよく表す。 二つの命題 P, Q に対する論理積を P ∧ Q と書き、「P かつ Q」や「P そして Q」などと読む。 ベン図による論理積P \wedge Q の表.
新しい！!: ユニフィケーションと論理積 · 続きを見る »
自動推論
自動推論（じどうすいろん、Automated Reasoning）は計算機科学と数理論理学の一分野であり、推論の様々な側面を理解することでコンピュータによる完全（あるいはほぼ完全）自動な推論を行うソフトウェアを開発することを目的とする。人工知能研究の一部と考えられるが、理論計算機科学や哲学とも深い関係がある。 自動推論のなかでも最も研究が進んでいるのは、自動定理証明（および完全自動ではないがより現実的な）と（固定の前提条件下での推論と見なすことができる）であるが、他にも類推、帰納、アブダクションによる推論の研究も盛んである。他の重要なトピックとしては、不確かさのある状況での推論と非単調推論である。不確かさに関する研究では論証（argumentation）が重要である。それはすなわち、標準的な自動推論へのさらなる極小性と一貫性の適用である。John Pollock の Oscar システムは単なる自動定理証明機よりも自動論証システムといえるものである。 自動推論のツールや手法としては、古典的論理学や代数学があるが、他にもファジィ論理、ベイズ推定、最大エントロピー原理に基づく推論、その他のあまり形式的でない技法などがある。.
新しい！!: ユニフィケーションと自動推論 · 続きを見る »
Haskell
Haskell（ハスケル）は非正格な評価を特徴とする純粋関数型プログラミング言語である。名称は数学者であり論理学者であるハスケル・カリーに由来する。.
新しい！!: ユニフィケーションとHaskell · 続きを見る »
Prolog
Prolog（プロログ）は、非手続き型プログラミング言語の一つ。論理型言語に分類される。名称は、「論理を使ったプログラミング」を意味するフランス語「programmation en logique」に由来しているRobert Kowalski.
新しい！!: ユニフィケーションとProlog · 続きを見る »
推移関係
推移関係（すいいかんけい、Transitive relation）は、数学における二項関係の一種。集合 X の二項関係 R が推移的であるとは、Xの任意の元 a、b、c について、a と b に R が成り立ち、b と c に R が成り立つとき、a と c にも R が成り立つことをいう。推移的関係とも。 一階述語論理でこれを表すと、次のようになる。.
新しい！!: ユニフィケーションと推移関係 · 続きを見る »
恒等式
恒等式（こうとうしき、identity）は、恒真な等式、すなわち等号 (.
新しい！!: ユニフィケーションと恒等式 · 続きを見る »
恒真式
恒真式（こうしんしき、トートロジー、tautology、ギリシャ語のταυτο「同じ」に由来）とは論理学の用語で、「aならば aである（a → a）」「aである、または、aでない（a ∨ ￢a）」のように、そこに含まれる命題変数の真理値、あるいは解釈に関わらず常に真となる論理式である。.
新しい！!: ユニフィケーションと恒真式 · 続きを見る »
束 (束論)
数学における束（そく、lattice）は、任意の二元集合が一意的な上限（最小上界、二元の結びとも呼ばれる）および下限（最大下界、二元の交わりとも呼ばれる）を持つ半順序集合である。それと同時に、ある種の公理的恒等式を満足する代数的構造としても定義できる。二つの定義が同値であることにより、束論は順序集合論と普遍代数学の双方の領域に属することとなる。さらに、半束 (semilattice) の概念は束の概念を含み、さらにハイティング代数やブール代数の概念も含む。これら束に関連する構造は全て順序集合としても代数系としても記述することができるという特徴を持つ。.
新しい！!: ユニフィケーションと束 (束論) · 続きを見る »
束縛 (情報工学)
束縛またはバインディング（Binding）は一般に、参照 (情報工学) の集合である。コンピュータ関連で「束縛」という語が使われるものはいくつかあり、それぞれ具体的な内容は異なるので、以下いくつかの例を示す。.
新しい！!: ユニフィケーションと束縛 (情報工学) · 続きを見る »
決定可能性
決定可能（けっていかのう、decidable）は、論理学において、論理式の集合のメンバーシップの決定をする実効的（effectiveな）方法が存在することを指す。決定可能性（けっていかのうせい、decidability）は、そのような属性を指す。命題論理のような形式体系は、論理的に妥当な論理式（または定理）の集合のメンバーシップを実効的に決定できるなら、決定可能である。ある決まった論理体系における理論（論理的帰結で閉じている論理式の集合）は、任意の論理式がその理論に含まれるか否かを決定する実効的方法があれば、決定可能である。.
新しい！!: ユニフィケーションと決定可能性 · 続きを見る »
数理論理学
数理論理学（mathematische Logik、mathematical logic）は、論理学（形式論理学）の数学への応用の探求ないしは論理学の数学的な解析を主たる目的とする、数学の関連分野である。局所的には数理論理学は超数学、数学基礎論、理論計算機科学などと密接に関係している。数理論理学の共通な課題としては形式体系の表現力や形式証明系の演繹の能力の研究が含まれる。 数理論理学はしばしば集合論、モデル理論、再帰理論、証明論の4つの領域に分類される。これらの領域はロジックのとくに一階述語論理や定義可能性に関する結果を共有している。計算機科学（とくに）における数理論理学の役割の詳細はこの記事には含まれていない。詳細はを参照。 この分野が始まって以来、数理論理学は数学基礎論の研究に貢献し、また逆に動機付けられてきた。数学基礎論は幾何学、算術、解析学に対する公理的な枠組みの開発とともに19世紀末に始まった。20世紀初頭、数学基礎論は、ヒルベルトのプログラムによって、数学の基礎理論の無矛盾性を証明するものとして形成された。クルト・ゲーデルとゲルハルト・ゲンツェンによる結果やその他は、プログラムの部分的な解決を提供しつつ、無矛盾性の証明に伴う問題点を明らかにした。集合論における仕事は殆ど全ての通常の数学を集合の言葉で形式化できることを示した。しかしながら、集合論に共通の公理からは証明することができない幾つかの命題が存在することも知られた。むしろ現代の数学基礎論では、全ての数学を展開できる公理系を見つけるよりも、数学の一部がどのような特定の形式的体系で形式化することが可能であるか（逆数学のように）ということに焦点を当てている。.
新しい！!: ユニフィケーションと数理論理学 · 続きを見る »
ここにリダイレクトされます：
単一化。
