このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

型推論に関わる論理の概念と用語 その1

寒いのがホントに苦手。寒いと活動レベルが下がって、なんもやる気が出ないわ。

これ、一回のエントリーで書こうとした内容なんだけど、途中までなので「その1」を付けました。中途半端なところでブチッと終りますが、続きをたぶん書きます。

[追記 date="2012-01-27"]「論理式の構成法」と「型の論理式」はこのエントリー内に続きを書きました。さらに続きは別なエントリーになるでしょう。[/追記] [追記 date="2012-01-30"]後に続く記事とツジツマをあわせるため、文言をわずかに修正。[/追記]


型推論を備えるプログラミング言語が増えてきましたね。そのうちに、型推論プログラミング言語の「普通の機能」になるのかもしれません。

型推論と一口にいっても、型システムとか計算モデルによって色々と違いが出るでしょうし、そもそも「型推論」て言葉が何を意味するかもそれほど明らかじゃないです。人によって使い方が違うのではないでしょうか。僕自身は、「型推論」は「型の演繹系の理論」と捉えています*1。同語反復みたいですけど(苦笑)。

演繹とは、論理的な推論・証明のことです。論理で使っている一般的な概念と用語に、形容詞「型」を付けると、それで型理論の対応する概念・用語になります。それで、論理の説明をするついでに型理論に触れるようなスタイルで、型推論の周辺を軽く紹介します。型概念としては、一番簡単な Sets-as-Types(型とは集合なり)を採用します。

内容:

シリーズ目次:

  1. その1 (この記事)
  2. その2
  3. その3
  4. その4
  5. その5
  6. その6
  7. 番外(型理論ってば)

項と論理式

論理では、式(expression)を二種類に分けるのが慣例です*2。例として、算術(小学校で習う数の四則計算)を考えます。2 + 3×4 のように「数を表す式」と、2 + 3×4 > 10 のような「主張や判断を表す式」に分けます。「数(に限らず対象物)を表す式」を項(term)、「主張や判断を表す式」を論理式(formula)と呼びます。

論理式を命題(proposition)と呼ぶこともあります。本来、論理式は構文的な概念で、命題だと意味も考えるのでしょうが、まーあんまり神経質にならずに、論理式と命題は同じと思っていいでしょう。僕は論理式と命題をほとんど区別していません。ついでに言うと、命題論理と述語論理の境界を引くのもあまり意味がないと思います(「論理とはなにか?」も参照)。

型理論では型が対象物なので、型を表す式が型項、型に関する主張や判断を表す式が型論理式、または型命題ということになります。

型項(type term)を type expression と呼ぶことは多いのですが、これを直訳すると「型式」、「ケイシキ」と読まれちゃうので、僕は「型表現」を使うことがあります。型表現と型項は同義語です。

項の構成法

項は次のような素材から組み立てます。

  1. 定数記号
  2. 変数記号
  3. 演算子記号
  4. 関数記号
  5. 補助記号(括弧類)

ここではいちいち「記号」と付けてますが、「定数記号」を単に「定数」のように呼ぶことが多いです。「○○記号」と「○○」は、ホントは違うのですが、これも神経質になると鬱陶しいので意図的に混同します。

例えば、(1 + sqrt(x))/2 という項の素材は:

  1. 定数記号: 1, 2
  2. 変数記号: x
  3. 演算子記号: +, /
  4. 関数記号: sqrt()
  5. 補助記号(括弧類): (, )

型に関しても、+ が直和、* が直積、string, boolean は基本的な型、Tが型変数とするなら、型項 string + string*boolean + list<T> の素材は:

  1. 型定数記号: string, boolean
  2. 型変数記号: T
  3. 演算子記号: +, *
  4. 型関数記号: list<>
  5. 補助記号(括弧類): 使ってない

演算子記号と関数記号の違いは書き方のスタイルだけなので、1 + 2 を sum(1, 2) に直すようにすると、関数記号だけにすることができます。この事情は型項のときも同じで、string + string*boolean + list<T> を型関数記号を使って、次のように書いてもかまいません。

  • sum<sum<string, prod<string, boolean>>, list<T>>

型関数の引数を囲むのに山形括弧(不等号の対)を使うのも単なる習慣で、丸括弧でも問題はありません。

  • sum(sum(string, prod(string, boolean)), list(T))

論理式の構成法

今日(2012-01-26)はここまで:たぶん、続く。



算術の 2 + 3×4 とか、変数を含んだ x + 1 とかは項です。それに対して、通常、方程式とか不等式とか呼ばれている式は論理式(formula)です。論理式を作るには、今までに出てきた記号類(定数記号、…、関数記号)とは別な種類の記号が必要です。それは関係記号です。例えば、等号「=」とか不等号「≦」なんかが関係記号です。

2 + 3×4 = 14 とか x + 1 ≦ 5 とかは関係記号を含んだ論理式です。関係記号は A = B とか A ≦ B のような中置(infix notation)にすることが多いですが、Eq(2 + 3×4, 14)、Le(x + 1, 5) のような関数っぽい書き方でもかまいません。

等号「=」と不等号「≦」は二項関係記号ですが、三項以上の関係記号や単項の関係記号があってもかまいません。例えば、「m は a と b の平均である」ということを Mean(m, a, b) と書けばMeanは三項関係記号です。「x は偶数である」を Even(x) と書けばEvenは単項関係記号です。

単項の関係は述語(predicate)と呼ぶことが多いので、単項関係記号は述語記号ともいいます。述語を関係と同義語として使う人もいます -- そのときは二項述語とか三項述語とかも出てきます。ここでは、単項のときは述語記号、二項以上なら関係記号と呼ぶことにします。また、関係記号/述語記号も、Eq(2 + 3×4, 14) のような関数っぽい書き方を標準とします。

論理式(命題)の一般的な作り方は次のようになります。

  • 述語記号(項)、二項関係記号(項1, 項2)、三項関係記号(項1, 項2, 項3) などを原子論理式と呼ぶ。
  • 原子論理式をベースに、論理結合記号により組み立てた式が論理式となる。

論理結合記号の選び方は目的や趣味により色々ですが、古典論理の標準的な論理結合記号である ∧(連言、かつ)、∨(選言、または)、¬(否定、ではない)、⊃(含意、ならば)としておきます。「論理記号のいろいろ」と「さまざまな「ならば」達」も参考にしてください。

2 + 3×4 = 14 と x + 1 ≦ 5 は原子論理式なので、(2 + 3×4 = 14) ∧ ¬(x + 1 ≦ 5) は原子論理式から組み立てられた論理式の例となります。

型の論理式

型に関する議論でも、項と論理式(命題)が出てきます。しかし、型の場合は、各種の記号類を2セット用意するのが普通です。なぜかというと、議論の対象物が二種類あるからです。ひとつはもちろん型、もうひとつの対象物は型に属するインスタンスデータです。Sets-as-Typesの立場なら、集合とその要素と言っても同じことです。

各種の記号類を2セット用意するなら、次のモノが必要です。

インスタンス
定数記号 型定数記号
変数記号 型変数記号
演算子記号 演算子記号
関数記号 型関数記号
述語記号 型述語記号
関係記号 型関係記号

項もインスタンス項と型項(型表現)があり、インスタンスに関する論理式と型に関する、あるいはインスタンスと型の両方に関する論理式があります。でも、論理結合子は共通に使えます。上の表では、「型○○」という単純な名称を使ってますが、型理論特有の言い回しがあります。例えば、型演算子とか型関数とか言うよりは、型構成子とか総称型と呼ぶことが多いでしょう。

型を含む論理式(命題)で一番よく使うのは、「インスタンス項 ∈ 型項」という形のものです。ここでは集合の所属関係の記号「∈」を使いましたが、コロン「:」のほうが利用例は多いでしょう。例えば、3∈integer (あるいは 3 : integer)とか、f(2, x)∈(integer + string) とかです(+ は直和、つまりユニオン型のつもり)。

インスタンスと型の二種類の対象物を扱う点と、論理とは違った固有の言葉使いがある点で、型推論は難しい印象があるのですが、普通の論理と違ったことをやるわけではありません。

今日(2012-01-27)はここまで:たぶん、続く。

*1:より広い概念としては、「型解析」という言葉を使っています。型解析には「型の計算」、「型の演繹」、「型の演繹系のメタ理論」があり、型の演繹のメタ理論≒型推論 です。

*2:分けない流儀もあります。