利用者:Foxtrot/翻訳/Haskell/カリー=ハワード同型

The Curry-Howard isomorphism is a striking relationship connecting two seemingly unrelated areas of mathematics — type theory and structural logic.

カリー=ハワード同型は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。

Introduction 導入

The Curry-Howard isomorphism, hereafter referred to as simply C-H, tells us that in order to prove any mathematical theorem, all we have to do is construct a certain type which reflects the nature of that theorem, then find a value that has that type. This seems extremely weird at first: what do types have to do with theorems? However, as we shall see, the two are very closely related. A quick note before we begin: for these introductory paragraphs, we ignore the existence of expressions like error and undefined whose denotational semantics are ⊥. These have an extremely important role, but we will consider them separately in due time. We also ignore functions that bypass the type system like unsafeCoerce#.

これよりカリー=ハワード同型は単に C-H と表記する。定理の本質を反映するような型を構築し、それからその型を持つ値を見つけさえすれば、どんな数学的定理をも証明することができる、ということをC-H が示している。これは最初は極めて不思議に思える。型と定理にどんな関係があるというのだろうか？しかしながら、以下に述べるように、このふたつは非常に近しい関係にあるのである。はじめる前に簡単に注意しておくが、導入の章では error や undefinedのような 表示的意味論 が ⊥ である式の存在は無視する。これらはとても重要な役割を果たすのだが、これらについては後ほど別に考えることにする。また、unsafeCoerce#のような型システムを迂回する関数についても無視することにする。

We can build incredibly complicated types using Haskell's higher-order functions feature. We might want to ask the question: given an arbitrary type, under what conditions does there exist a value with that type (we say the type is inhabited)? A first guess might be 'all the time', but this quickly breaks down under examples. For example, there is no function with type a -> b, because we have no way of turning something of type a into something of a completely different type b (unless we know in advance which types a and b are, in which case we're talking about a monomorphic function, such as ord :: Char -> Int).

Haskellの高階関数の機能を使えばとても複雑な型を構築することができる。次のような質問をしてみるといい。すべての型は少なくともひとつは値が存在する(このような型を空でない集合(inhabited)という)だろうか？最初は「どんな型でもそうだ」と思うかもしれないが、次の例はあっさりとその直感を打ち砕く。たとえば、なんらかの型aの値をまったく別の型 b の値に変換する方法は存在しないので(あらかじめ a や bを知っており ord :: Char -> Intのような単相関数について述べているのでない限り)、型a -> bをもつ関数は存在しない。

Incredibly, it turns out that a type is only inhabited when it corresponds to a true theorem in mathematical logic. But what is the nature of this correspondence? What does a type like a -> b mean in the context of logic?

信じられないことに、型が数学の論理における真である定理と対応するときだけ、型は空でないことがわかるのである。しかし、この対応はなぜなのだろうか？a -> bのような型は論理の文脈においては何を意味しているのだろうか？

A crash course in formal logic 形式論理最速入門

We need some background on formal logic before we can begin to explore its relationship to type theory. This is a very brief introduction; for a wider grounding we recommend you consult an introductory textbook on the subject matter.

型理論の探求を始める前に、ある程度の形式論理の素養が必要だ。これはとても簡単な入門である。より詳しい背景を知るためには、形式理論についての入門書を参照することをお勧めする。

In everyday language we use a lot of 'If... then...' sentences. For example, 'If the weather is nice today, then we'll walk into town'. These kinds of statements also crop up in mathematics; we can say things like 'If x is positive, then it has a (real) square root'. Formal logic is a way of translating these statements from loose, woolly, ambiguous English into precise symbolism. We use the → sign (read as 'implies') to indicate that something is true if something else is true. For example, our earlier statement could be recast as 'The weather is nice today → we'll walk into town', which means that it is true that we'll walk into town if it is true that the weather is nice, which is just the same as the 'If... then...' version we used earlier. We'll often use letters to stand for entire statements, so for example if W is the statement 'the weather is nice', and T is the statement 'we'll walk into town', then our example becomes simply W → T.

我々は毎日のように「もし～ならば～」という表現を使っている。たとえば、「もし天気が良かったら、街まで歩いていく」などだ。この種の表現は数学にも登場する。「もしxが正なら、xは(実数の)平方根を持つ」のように言うことがあるだろう。形式論理は曖昧でぼんやりとした自然言語を正確な記号へとこのような主張を翻訳する手段なのである。もし何かが真なら真であるということを、 → 記号(「ならば」と読む)を使って表す。例えば、もし天気が良いということが真なら、街まで歩いて行くというのが真である、という先程使った「もし～ならば～」による文章とまったくおなじ意味で、先ほどの文章は「天気が良い→街まで歩いて行く」と書き換えることができる。また、文章全体を表すために文字を使うことがある。たとえば、もし W が先程の「天気がいい」という文章で、Tが「街まで歩いて行く」という文章なら、先程の例は単に W →T と書ける。

Notice the crafty way we phrased our definition of →. P → Q means that if P is true, then Q is true. But if Q is some statement that is always true, no matter what the circumstances — like 'the sun is hot' — then it doesn't matter what P is. P could even be a false statement, Q would still be true if P were true, so P → Q would still hold. The fact that Q would be true if P isn't true is a whole different matter; we're not asking that question when we say P → Q. So → doesn't really represent any kind of cause-effect relationship; things like 'the sky is pink → the sun is hot' are still valid statements.

先程述べた → の定義のずるい方法に注意されたい。P → Q は、もし P が真なら、 Qは真である、という意味だった。でも、もし Qが「太陽は熱い」のような常に真であるような文章だったら、Pが何であっても問題はない。Pが偽である文章だとしても同様で、もしPが真であったとしても Qは真であるということになる。したがって、P → Qはやはり成り立つ。Pが真でなくとも Q が真になるということは、まったく別のことなのだ。P → Qといった時にこの疑問を尋ねることはない。よって、「空が赤い→太陽は熱い」がやはり正当な文章であるように、→は実はなんらかの因果関係の一種を表しているわけではない。

Other things that crop up lots in both everyday language and mathematics are things called conjunctions and disjunctions. The former represent statements involving an 'and', the latter statements involving an 'or'. We could represent the statement 'I will buy this magazine if it's in stock and I have enough money' by the symbolism $(M\wedge S)\to B$, where M = 'I have enough money', S = 'The magazine is in stock', B = 'I will buy the magazine'. Essentially, one can just read the symbol $\wedge$ as 'and'. Similarly, one can read the symbol $\vee$ as 'or', so that the statement 'I will either walk or get the train to work' could be represented as $W\vee T$, where W = 'I will walk to work', and T = 'I will get the train to work'.

論理積と論理和と呼ばれるものも日常の言語と数学の両方で登場する事柄である。前者は「かつ」、後者は「または」を意味する形式表現である。「もし在庫がありお金が足りれば、この雑誌を買うだろう」という文章は形式的に$(M\wedge S)\to B$と表現される。ここで、M = 'お金が足りる'、S = '雑誌の在庫がある'、B = '雑誌を買うだろう'である。実際、$\wedge$単には「かつ」と読むことができる。同様に、$\vee$ は「または」と読むことができ、「徒歩か電車で仕事に行くだろう」は$W\vee T$と表される。ここで、W = '徒歩で仕事に行く', and T = '電車で仕事に行く'である。

Using these symbols, and a few more which will be introduced as we go, we can produce arbitrarily complicated symbol strings. There are two classes of these symbol strings: those that represent true statements, often called the theorems; and those which represent false statements, called the nontheorems. Note that whether a symbol string is a theorem or nontheorem depends on what the letters stand for, so $P\vee Q$ is a theorem if, for example, P represents the statement 'It is daytime' and Q represents the statement 'It is night time' (ignoring exceptions like twilight), but it would be a nontheorem if P were 'Trees are blue' and Q were 'All birds can fly'. We'll often call a symbol string a proposition if we don't know whether it's a theorem or not.

これらの記号とこれから紹介する幾つかのものを使い、任意の複雑な記号列を生成することができる。これらの記号列は、定理(theorems)と呼ばれることもある真の主張と、非定理(nontheorems)と呼ばれることがある偽の主張の二種類に分類できる。あらゆる記号列はその文字が表しているものに従って定理か非定理のどちらかになることに注意すると、例えば、もし P が「昼間である」という文章を表し、Qが「夜である」という文章を表すなら、(夕方のような例外を除けば)$P\vee Q$ は定理であるが、もしPが「木は青い」でQは「すべての鳥は飛ぶことができる」ならこれは非定理となる。定理かどうかわからない記号列は、命題と呼ぶこともある。

There are many more subtleties to the subject of logic (including the fact that when we say 'If you eat your dinner you'll get dessert' we actually mean 'If and only if you eat your dinner will you get dessert'). If this is a subject that interests you, there are many textbooks around that comprehensively cover the subject.

(「もしあなたが夕食を食べるのなら、その時に限りデザートを食べるだろう」という意味で「もしあなたが夕食を食べるならデザートも食べるだろう」というときのように)論理にはもっと多くの微妙な話題が存在する。もしこれらの話題に興味があるなら、これらの話題を包括的にあつかう多くの教科書がある。

Propositions are types 定理と型

So, given a type a -> b, what does that mean in terms of symbolistic logic? Handily, it simply means that a → b. Of course, this only makes sense if a and b are types which can further be interpreted in our symbolistic logic. This is the essence of C-H. Furthermore, as we mentioned before, a → b is a theorem if and only if a -> b is an inhabited type.

それでは、形式論理においては型 a -> b は何を意味するのだろうか？簡単なことに、単にa → bを意味しているのだ。もちろん、これはa と bが形式理論において解釈可能な型であるときだけ成り立っている。これは C-H の本質である。また、先程述べたように、a -> b が空でない型であるとき、その時に限り a → bは定理となる。

Let's see this using one of the simplest of Haskell functions. const has the type a -> b -> a. Translated into logic, we have that a → b → a. This must be a theorem, as the type a -> b -> a is inhabited by the value const. Now, another way of expressing a → b is that 'If we assume a is true, then b must be true.' So a → b → a means that if we assume a is true, then if we further assume that b is true, then we can conclude a. This is of course a theorem; we assumed a, so a is true under our assumptions.

もっとも単純な Haskell 関数のひとつを使ってみていこう。const は a -> b -> a　という型を持つ。形式論理ではa → b → aとなる。値constがあるので、これは型 a -> b -> a が空ではなく、定理であることは間違いない。いま、a → bは「もしa が真だとすれば、b は真である」の別の表現なのである。したがって、a → b → a は「もしaが真であり、もしbが真であるなら、aは真であると結論できることを意味する。aが真であると仮定するなら、仮定によりaが真であるから、これはもちろん定理である。

The problem with ⊥ ⊥にまつわる問題

We've mentioned that a type corresponds to a theorem if that type is inhabited. However, in Haskell, every type is inhabited by the value undefined. Indeed, more generally, anything with type forall a. a, a value with denotational semantics of ⊥, is a problem. ⊥ in type theory corresponds to inconsistency in logic; we can prove any theorem using Haskell types because every type is inhabited. Therefore, Haskell's type system actually corresponds to an inconsistent logic system. However, if we work with a limited subset of Haskell's type system, and in particular disallow polymorphic types, we have a consistent logic system we can do some cool stuff in. Hereafter it is assumed we are working in such a type system.

型が空でないならば、その型は定理と一致することを述べてきた。しかしながら、Haskell においては、値undefinedが存在することにより、どんな型も空ではない。実際に、より一般的には、⊥の表示的意味論を持つ値は、すべては型forall a. aという型であるのが問題なのである。型理論における⊥は、論理における矛盾と一致する。すべての型は空でないので、Haskell の型を使ってどんな定理も証明することができる。それゆえ、Haskell の型システムは実際には矛盾した論理システムと一致する。しかしながら、もしHaskellの型システムの制限されたサブセットを使うなら、特に多相型を禁止すれば、ちゃんと面白いことができる一貫性のある論理体系を得ることができる。これからは、そのような型システム内で話を進めていく。

Now that we have the basics of C-H, we can begin to unpack a little more the relationship between types and propositions.

これで C-H の基礎を身に着けたので、型と命題の関係をさらに解き明かすのを始めることができるようになった。

Logical operations and their equivalents 論理演算と等価なもの

The essence of symbolic logic is a set of propositions, such as P and Q, and different ways of combining these propositions such as Q → P or $P\vee Q$. These ways of combining propositions can be thought of as operations on propositions. By C-H, propositions correspond to types, so we should have that the C-H equivalents of these proposition combinators are type operations, more normally known as type constructors. We've already seen an example of this: the implication operator → in logic corresponds to the type constructor (->). The rest of this section proceeds to explore the rest of the proposition combinators and explain their correspondence.

記号論理の本質は、P や Qのような命題の集合と、Q → P or $P\vee Q$のようなこれらの命題を組み合わせるさまざまな方法である。命題を組み合わせるこれらの方法は命題の演算と考えることができる。C-H により命題は型と対応し、ゆえに普通は型構築子として知られるその論理演算とC-Hの等価なものを得るのである。すでにこの一例を見てきた。論理における論理包含演算子→は型構築子(->)と対応する。この章の残りの部分は残りの命題演算を探求し、対応関係の説明を進めていく。

Conjunction and Disjunction 論理積と論理和

In order for $A\wedge B$ to be a theorem, both A and B must be theorems. So a proof for $A\wedge B$ amounts to proving both A and B. Remember that to prove a proposition A we find a value of type A, where A and A are C-H correspondents. So in this instance we wish to find a value that contains two sub-values: the first whose type corresponds to A, and the second whose type corresponds to B. This sounds remarkably like a pair. Indeed, we represent the symbol string $A\wedge B$ by (a, b), where a corresponds to A and b corresponds to B.

$A\wedge B$が定理となるためには、A と B の両方は定理でなければならない。よって、$A\wedge B$ の証明はAと Bの両方を証明することに等しい。型Aの値を見つけることが 命題 A の証明であることを思い出そう。ここで A とA は C-H 対応している。ゆえに、この場合、最初のAと一致する型と２つ目のBと一致する型の、従属する２つの値含む値を見つけたいということになる。これは実にペアに似ているように思える。実際に、記号列$A\wedge B$は(a, b)と表現する。ここでa はA に、b は Bに相当する。

Disjunction is opposite to conjunction. In order for $A\vee B$ to be a theorem, either A or B must be a theorem. Again, we search for a value which contains either a value of type A or a value of type B. This is Either. Either A B is the type which corresponds to the proposition $A\vee B$.

論理和は論理積とは逆である。$A\vee B$ が定理であるためには、A かBのどちらかが定理でなければならない。先程と同様に、型Aの値か型Bの値のどちらかを含むような値を探す。これは Eitherだ。Either A B は命題 $A\vee B$と一致する型なのである。

Falsity 偽

It is occasionally useful to represent a false statement in our logic system. By definition, a false statement is one that can't be proven. So we're looking for a type which isn't inhabited. Although none of these types exist in the default libraries (don't get confused with the () type, which has precisely one value), we can define one, if we turn on the -XEmptyDataDecls flag in GHC:

我々の論理体系では、偽の主張を表すことは役に立つことがある。定義により、偽の主張は証明することができないものである。ゆえに、空であるような型を探すことになる。デフォルトのライブラリにはこのような型は存在しないが(()型で混乱しないように。これは明らかにひとつ値がある)、GHC の -XEmptyDataDeclsフラグをオンにすれば自分で定義することができる。

data Void

The effect of omitting the constructors means that Void is an uninhabited type. So the Void type corresponds to a nontheorem in our logic. There are a few handy corollaries here:

構築子を省くことにより、Void は空である型を意味することになる。それゆえ、Void 型は論理の非定理と一致する。役に立つ当然の帰結を幾つか挙げる。

1. (Void, A) and (A, Void) are both uninhabited types for any type A, corresponding to the fact that $F\wedge A$ and $A\wedge F$ are both nontheorems if F is a nontheorem. どんな型Aについても、(Void, A) と (A, Void) はどちらも空である型であり、もしFが非定理なら $F\wedge A$ と $A\wedge F$ はどちらも非定理であるという事実と対応する。
2. Either Void A and Either A Void are essentially the same as A for any type A, corresponding to the fact that $F\vee A$ and $A\vee F$, where F is a nontheorem, are theorems only if A is a theorem. どんな型Aについても、Either Void A と Either A Void は本質的に A と同じであり、 Fが非定理で A が定理であるとき、$F\vee A$ と $A\vee F$が真であるという事実と対応する。
3. Any type that corresponds to a nontheorem can be replaced with Void. This is because any nontheorem-type must be uninhabited, so replacing it with Void everywhere doesn't change anything. Void is really equivalent to any nontheorem type. 非定理と対応するどんな型もVoidに置き換えることができる。これはどんな非定理型も空であるからで、ゆえになにも変更せずともVoidに置き換えることができるのである。Void は実際にどんな非定理型とも等価である.

4. As we remarked in the first section, the implication P → Q is true if Q is true, regardless of the truth value of P. So we should be able to find a term with type Void -> a. In fact one does exist, but it's somewhat complicated to explain: the answer is the empty function. We can define a function f :: A -> B as a (probably infinite) set of pairs whose first element is an element of A (the domain) and second element is f's output on this term, an element of B (the range). For example, the successor function on the naturals is represented as {(0,1), (1,2), (2,3), ...}. Note that in order to be a (total and well-defined) function, we must have precisely one pair (a, f a) for each term a with type A.

   最初の章で発見したように、Pの値が真であるかどうかにかかわらず、もしQが真であれば論理包含 P → Q は真である。したがって、型 Void -> a の項を見つけ出すことができるはずである。実際に存在するのだが、これはすこし説明が複雑になる。答えは 空(empty)関数である。関数 f :: A -> B を 最初の要素が Aの要素であるような(おそらく無限の) 集合の組 (定義域) と ２つ目の要素がB (値域)の要素であるようなこの項におけるfの出力と定義することができる。たとえば、自然数においてある自然数のすぐ次の自然数を得る関数は{(0,1), (1,2), (2,3), ...}と表すことができる。(total かつ well-defined な) 関数とするために、項 aが型Aである組 (a, f a)ひとつをちょうど得ることに注意されたい。

   The empty function, let's call it empty is represented in this way by the empty set. But as we must have a pair for each element of the domain, and there no pairs in our representation, the domain type must be empty, i.e. Void. What about the range type? empty never produces any output, so there are no restrictions placed on the range type. Thus, it is valid to assume that the range type has any type, so we can say empty :: forall a. Void -> a. Unfortunately, it's not possible to write this function in Haskell; we'd ideally like to write something like:

   この空関数をempty と呼ぶことにしよう。このようにemptyは空集合で表すことができる。 しかし、それぞれ定義域の要素である組がなければならないが、この表現に組は存在せず、定義域は空、すなわち Void でなければならない。値域の型についてはどうだろうか。empty はどんな出力もしないので、値域に課された制限はない。それゆえ、値域の型はどんな型と仮定しても正当であり、empty :: forall a. Void -> aということになる。残念ながら Haskell ではこのような関数を書くことはできないが、理想的には次のように書ければよい。

   
   

   empty :: Void -> a
   

   And stop there, but this is illegal Haskell. The closest we can come is the following:

   これは Haskell では禁じられている。なんとか可能そうなもっとも近いものは次のようなものだ。

   empty :: Void -> a
   empty _ = undefined
   

   Alternatively:

   もしくは、

   empty :: Void -> a
   empty = empty
   

   Another reasonable way (also disallowed in Haskell) would be to write:

   (やはりHaskellでは許されないのだが)ほかの理にかなった方法としては次のように書くことが考えられる。

   empty x = case x of { }
   

   The case statement is perfectly well formed since it handles every possible value of x.

   これはどんなxの値も扱うことができるので、このcase 文は完全に適切な形式(well formed)である。

   Note that this is perfectly safe, since the right-hand side of this function can never be reached (since we have nothing to pass it). So, the conclusion of all this is that Void -> a is an inhabited type, just as P → Q is true if P is false.

   関数の右辺には決して届かない(ゆえに何も渡してはいない)ので、これはまったく安全であることに注意しよう。全体の結論としては、Void -> a は空でない型であり、P が偽であるならばP → Q は真である、ということになる。

Negation 否定

The ¬ operation in logic turns theorems into nontheorems and vice versa: if A is a theorem then ¬A is a nontheorem; if A is a nontheorem then ¬A is a theorem. How can we represent this in Haskell? The answer's a sneaky one. We define a type synonym:

論理のおける ¬ 演算は、定理を非定理に、非定理を定理に変える。もし A が定理なら ¬A は非定理であるし、A が非定理なら ¬A は定理となる。Haskell ではどうやって表現できるだろうか？回答はずるいものだ。型シノニムを定義する。

type Not a = a -> Void

So for a type A, Not A is just A -> Void. How does this work? Well, if A was a theorem-type, then A -> Void must be uninhabited: there's no way any function could return any value, because the return type, Void has no values (The function has to provide values for all inhabitants of A)! On the other hand, if A was a nontheorem, then A can be replaced with Void as we explored in the last section. Then the function id :: Void -> Void is an inhabitant of Not A, so Not A is a theorem as required (The function doesn't have to provide any values, since there are no inhabitants in its domain. Nevertheless it's a function — with an empty graph).

だから、Aについて、Not Aの型は単にA -> Voidである。これはどのように働くのだろう？ A が定理型であれば、 A -> Void は空でない集合でなければならない。返り値の型 Void は値を持っていないので、どんな関数もどんな値でも返す方法はない(この関数は A のすべての空でない集合についても値を提供しているはずである)！言い換えれば、先ほどの章で探求したように、A が非定理だったら、AをVoidに置き換えることができる。そして、関数　id :: Void -> Void　はNot Aの要素であり、ゆえに要求通りNot Aは定理となる(その定義域に要素がないので、この関数はどんな値も提供する必要はない。それにもかかわらず、これは空のグラフであり、関数なのだ。)。

Axiomatic logic and the combinatory calculus 公理的論理と組み合わせ計算

So far we've only used some very basic features from Haskell's type system. Indeed, most of the features of logic we've mentioned can be explored using a very basic 'programming language', the combinator calculus. To fully appreciate how closely C-H ties together these two areas of mathematics, we need to axiomatise both our discussion of formal logic and our discussion of programming languages.

これまでのところ、Haskell の型システムからいくつかのごく基本的な機能のみを使ってきた。論理のほとんどの機能はごく基本的な「プログラミング言語」であるコンビネータ計算(combinator calculus)を使えば探求することができる。どうやってC-H がこれらの２つの領域を結びつけているかを十分に理解するためには、形式論理の議論とプログラミング言語についての議論の両方を「公理化」する必要がある。

Axiomatic logic 公理的論理

We start with two axioms about how the → operation should behave (from now on, we assume that → is a right-associative function, i.e. A → B → C means A → (B → C)):

→操作がどのように振る舞うべきかについてのふたつの公理から始めよう(いまから、これらの → は右結合関数である、すなわち、A → B → C は A → (B → C) を意味するものとする)。

1. A → B → A
2. (A → B → C) → (A → B) → A → C

The first axiom says that given any two propositions A and B, if we assume both A and B, we know that A is true. The second says that if A implies that B implies C (or equivalently, if C is true whenever A and B are true), and A itself implies B, then knowing A is true would be enough to conclude that C is true. This may seem complicated, but a bit of thought reveals it to be common sense. Imagine we have a collection of boxes of various colours, some with wheels, some with lids, such that all the red boxes with wheels also have lids, and all the red boxes have wheels. Pick one box. Let A = 'The box under consideration is red', B = 'The box under consideration has wheels', C = 'The box under consideration has a lid'. Then the second law tells us that, as A → B → C (all red boxes with wheels also have lids), and A → B (all red boxes have wheels), then if A (if the box is red), then C must be true (the box has a lid).

最初の公理は、どんな２つの命題 A と B についても、もし A と B の両方を仮定するなら、A が真であるということがわかる、ということを言っている。ふたつめの公理は、もし A ならば B ならば C ならば(言い換えれば、もし C が真ならいつも A と B も真であるとすれば)、かつ A ならば B であれば、A が真であることがわかれば C が真であると結論できるということだ。これは複雑に見えるが、少し考えるとこれはごく当たり前のことであるのがわかる。様々な色の箱があり、車輪の付いているものや、蓋の付いているものもあると想像してみよう。すべての赤い車輪のついた箱には蓋があり、赤い箱には車輪がついている。ひとつ箱を選ぶ。A = '検討中の箱は赤', B = '選んだこの箱は車輪が付いている', C = '選んだ箱には蓋が付いている'としよう。ふたつめの法則は、A → B → C (すべての赤い車輪がついている箱は蓋もついている)、かつ A → B (すべての赤い箱は車輪がついている)なら、もし A (箱が赤である)ならば、C (箱には蓋が付いている)が真であるのは間違いない。

We also allow one inference law, called modus ponens:

モーダス・ポネンスとも呼ばれている推論規則も認めることにする。

1. If A → B, and A, then B.　もし A → B　かつ A　なら、 B　である。　

This law allows us to create new theorems given old one. It should be fairly obvious; it is essentially the definition of what → means. This small basis provides a simple enough logic system which is expressive enough to cover most of our discussions. Here's a sample proof of the law A → A in our system:

この法則はもとの定理から新しい定理を作ることを可能にする。これはまったく明白のはずである。→ が何を意味しているかの本質的な定義そのものである。この小さな原理は、ほとんどの我々の議論をカバーする十分な表現力する、単純で十分な論理体系を提供する。このシステムにおける、A → Aの証明例を示す。

Firstly, we know the two axioms to be theorems:

最初に、定理としてふたつの公理を知っている。

• A → B → A
• (A → B → C) → (A → B) → A → C

You'll notice that the left-hand side of the second axiom looks a bit like the first axiom. The second axiom guarantees that if we know that A → B → C, then we can conclude (A → B) → A → C. In this case, if we let C be the same proposition as A, then we have that if A → B → A, then (A → B) → A → A. But we already know A → B → A, that was the first axiom. Therefore, we have that (A → B) → A → A is a theorem. If we further let B be the proposition C → A, for some other proposition C, then we have that if A → C → A, then A → A. But, again, we know that A → C → A (it's the first axiom again), so A → A, as we wanted.

ふたつめの公理の左辺が最初の公理であるように見えるのに気づくだろう。ふたつめの公理は、もしA → B → Cがわかっているなら、(A → B) → A → Cと結論できることを保証する。このとき、もし C を A と同じ命題だとすれば、もし A → B → Aならば (A → B) → A → A を得る。もし B を命題 C → A とすれば、ほかの命題 C について、もし A → C → A ならば A → A を得る。しかし、繰り返すが、A → C → A (これはまた最初の公理だ)であり、ゆえに求めていた A → Aを得る。

This example demonstrates that given some simple axioms and a simple way to make new theorems from old, we can derive more complicated theorems. It may take a while to get there — here we had several lines of reasoning to prove just that the obvious statement A → A is a theorem! — but we get there in the end. This kind of formalisation is attractive because we have essentially defined a very simple system, and it is very easy to study how that system works.

この例の実演はいくつかの単純な公理ともとの定理から新たな定理を創りだす簡単な方法さえあれば、さらに複雑な定理を導出できることを示す。これを得るまでに随分手間がかかるかもしれない。A → A が定理であるという明らかな主張を証明するのにも何行もかかった！しかし、最終的にはたどり着いた。本質的にごく簡単なシステムを定義し、このシステムがどのように働くのかを研究するのは非常に簡単なので、この種の形式化は興味深い。

Combinator calculus コンビネータ計算

The lambda calculus is a way of defining a simple programming language from a very simple basis. If you haven't already read the chapter that was just linked to, we recommend you read at least the introductory sections on the untyped version of the calculus. Here's a refresher in case you're feeling dusty. A lambda term is one of three things:

ラムダ計算はごく簡単な原理から単純なプログラミング言語を定義する方法のひとつである。もしまだラムダ計算の章を読んでいないのであれば、少なくとも型なしバージョンの計算の導入の節だけでも読んでおくことを勧める。忘れかけているかもしれないから、念のため確認しておこう。ラムダ項はつぎの３つのうちのひとつである。

• A value, v. 値, v
• A lambda abstraction $\lambda x.t$, where t is another lambda term. ラムダ抽象 $\lambda x.t$。ここで t は別のラムダ項である。
• An application $(t_{1}t_{2})$, where $t_{1}$ and $t_{2}$ are lambda terms. 適用 $(t_{1}t_{2})$。ここで $t_{1}$ と $t_{2}$ はどちらもラムダ項である。

There is one reduction law, too, called beta-reduction:

ベータ簡約 と呼ばれる簡約規則がひとつある。

• $((\lambda x.t_{1})t_{2})$ → $t_{1}[x:=t_{2}]$, where $t_{1}[x:=t_{2}]$ means $t_{1}$ with all the free occurrences of x replaced with $t_{2}$.　$((\lambda x.t_{1})t_{2})$ → $t_{1}[x:=t_{2}]$。ここで、$t_{1}[x:=t_{2}]$はすべての x の自由な出現をともなう$t_{1}$は$t_{2}$で置換されることを意味する。

As mentioned in the lambda calculus article, the difficulty comes when trying to pin down the notion of a free occurrence of an identifier. The combinator calculus was invented by the American mathematician Haskell Curry (after whom a certain programming language is named) because of these difficulties. There are many variants on the basic combinator calculus, but we consider one of the simplest here. We start with two so-called combinators:

ラムダ計算の項目で言及したように、識別子の自由な出現の記述を束縛するのを試すときには困難が生じる。これらの困難のため、コンビネータ計算はアメリカの数学者ハスケル・カリーによって考案された(のちにプログラミング言語の名前ともなった)。基本的なコンビネータ計算にはいくつかの亜種が存在するが、ここでは最も簡単なものについて考える。ふたつのいわゆる コンビネータ と呼ばれるものから始める。

• K takes two values and returns the first. In the lambda calculus, $\mathbf {K} =\lambda xy.\ x$.　K はふたつの値をとり、最初のひとつを返す。ラムダ計算においては、$\mathbf {K} =\lambda xy.\ x$　である。
• S takes a binary function, a unary function and a value, and applies that value and the value passed into the unary function to the binary function. again, in the lambda calculus: $\mathbf {S} =\lambda xyz.\ xz(yz)$. S は２引数の関数、１引数の関数、値をとり、値を１引数の関数に渡して、２引数の関数に適用する。ラムダ計算では、$\mathbf {S} =\lambda xyz.\ xz(yz)$ である。

The first function you should recognise as const. The second is more complicated, it is the monadic function ap in the ((->) e) monad (which is essentially Reader). These two combinators form a complete basis for the entire lambda calculus. Every lambda calculus program can be written using just these two functions.

最初の関数はconstだと認識したかもしれない。ふたつめはすこし複雑だが、((->) e) モナド(つまりは Reader だ)におけるモナディック関数 ap　である。これらふたつのコンビネータはラムダ計算全体の完全な基礎を形成する。どんなラムダ計算プログラムもこれらふたつの関数だけを使って書くことができる。

Intuitionistic vs classical logic 直観論理か古典論理か

So far, all of the results we have proved are theorems of intuitionistic logic. Let's see what happens when we try to prove the basic theorem of classical logic, Not Not A -> A . Recall that this translates as ((A -> Void) -> Void) -> A . So, given a function of type (A -> Void) -> Void we need a function of type A. Now a function of type (A -> Void) -> Void exists precisely if type A -> Void is uninhabited, or in other words if type A is inhabited. So we need a function which takes any inhabited type, and returns an element of that type. Although it is simple enough to do this on a computer - we need only find the "simplest" or "first" inhabitant of each type - there is no way to do this using standard lambda-calculus or combinator techniques. So we see that this result cannot be proved using these two techniques, and hence that the underlying logic is intuitionistic rather than classical.

これまで証明してきたすべての結果は、直観主義論理の定理である。古典論理の基本的な定理、 Not Not A -> A を証明することを試みるどうなるのであろうか。 ((A -> Void) -> Void) -> A と変換されることを思い出そう。すると、型 (A -> Void) -> Void の関数について 型Aを返すような関数が必要だ。いま、もし型 A -> Void が空である、言い換えれば 型 A が空であるなら、型 (A -> Void) -> Void の関数がまさに存在する。必要なのはなんらかの空である型をとりその型の要素を返す関数である。それぞれの型の "最も単純"、言い換えれば "最初" の要素を発見するだけであるので、コンピュータにとってはじゅうぶんに容易い。しかし、通常のラムダ計算やコンビネータの技法を使用してこれを果たす方法はない。ゆえに、これらの２つの技法を使ってこの結果を証明することができず、根本的な論理は古典論理というより直観論理であることがわかる。

Instead, consider a traditional error handling function which calls throw when an error occurs, transferring computation to catch. The throw function cancels any return value from the original function, so it has type A -> Void, where A is the type of its arguments. The catch function then takes the throw function as its argument, and, if the throw triggers (i.e. returns a Void) will return the argument of the throw function. So the type of catch is ((A -> Void) -> Void) -> A .

代わりに、エラーが発生した時に throwを呼び出しcatchへ計算を移行する、従来のエラー処理関数を考える。 throw関数はもとの関数のどんな返り値も取り消すので、その型は A -> Void である。ここで、A はその関数の引数の型である。catch 関数は throw 関数をその引数としてとり、もし throw が例外を引き起こす(すなわち Void を返す)なら throw 関数の引数を返すだろう。そして catch の型は ((A -> Void) -> Void) -> A となる。

Notes

テンプレート:Haskell navigation