2003-11-09 [長年日記]
λ. 衆議院選挙
投票してきた。
λ. 「メタ」と「高階」
これを読んで気になったのだけど、私は「高階(higher-order)」の「階(order)」って『A,Bのorderをm,nとすると、「Aに依存したB」のorderは max(m+1,n)』という条件で定義される数だと漠然と思ってたのだけど、これって正しいだろうか? 幾つか例を考えてみる。
λ. (例1) 関数
(関数でない通常の)値を0階の関数と考える。通常の関数は値に依存した値だから、max(0+1,0) = 1 より1階の関数。引数が一階の関数であるような関数は max(1+1,0) = 2 より二階の関数。二階以上の関数をまとめて高階関数と呼ぶ。
この定義だと引数が通常の値で返り値が一階の関数であるような関数は、max(0+1, max(0+1,0)) = 1 から一階の関数になってしまい、ちょっと直感に反する気もする。でも、カリー化によって階が変わらないのは逆に本質を捉えている気もする。
λ. (例2) 命題と論理
真偽値を0階の命題と考える。一階の命題は通常の命題。一階の命題に依存して真偽値が定まるような命題は max(1+1,0) = 2 より二階の命題。一階の命題と二階の命題の両方を扱う論理体系は二階論理、orderに制限のない論理体系は高階論理。
λ. (例3) 算術
真偽値を0階の対象と考える。一階の対象は自然数。自然数の集合は(特性関数によって「自然数に依存した真偽値」と考えられるので)二階の対象。自然数を扱う「Q」や「ペアノ算術」等の体系は一階の算術ともいわれる。自然数と自然数の集合の両方を対象とするZ2等の体系は二階算術といわれる。
λ. (例4) 型
「data Bool = True | False」で定義される型Boolのような引数を持たない型は一階の型。「data List X = Nil | Cons X (List X)」で定義されるような型は一階の型を引数に取るので二階の型。「data Fix f = In (f (Fix f))」で定義されるようなFixは二階の型を引数に取るので三階の型(?)。
ポリモルフィック・ラムダ計算(polymorphic lambda calculus) が、二階ラムダ計算(second-order lambda calculus)と呼ばれるのは二階の型を扱えるから?
λ. 高階型?
それはそうと「型の型」と言うと普通は「種(kind)」のことで、型をパラメータにとる型という意味での「高階型」とは違う気がします。
