オーブン料理は簡単でよい。手間をかけずに調理できるのにもかかわらず、食卓に並べたときは高級感を醸し出してくれる。このギャップを料理人は楽しむことができる。経済的な言葉を用いれば、費用対効果に優れているということだろう。でも、良いことばかり…

７．９ カリー＝ハワード同型対応 世の中には、言い方は違っているのだが、同じことを言っているということが往々にしてある。前回の記事で、型定理と圏論は一対一に対応づけできると説明したが、その例の一つである。さらに、もう一つ対応するものがある。…

７．８ 具体例 指数対象\(A^{B+C} = A^B \times A^C\)は、Haskellの型シグネチャで表すと、 \begin{eqnarray} Either \ b \ c \rightarrow a \sim (b \rightarrow a, c \rightarrow a) \end{eqnarray} となることを前回の記事で説明した。それでは、この型シ…

７．７ 型定理(Type Theory) 型定理という言葉に戸惑う人も多いことと思う。日本語版のウィキペディアで型理論を検索するとあまりにも短い記述にがっかりするだろう。得られる情報も余りない。しかし、さすがに英語版の方には詳しく書いてある。その記述の中…

７．６ 指数対象 写像対象には別の表現法がある。また、こちらの方がよく知られてもいる。それは指数対象と呼ばれる。対象\(A\)から対象\(B\)への射の集まり\(A \Rightarrow B\)を写像対象と呼んだ。同じように射の集まりなのだが、ドメイン\(A\)を肩に、コ…

７．３ 写像対象とは ここでは写像対象を定義することにしよう。前回の記事で写像対象を説明するための図として下図を提示した。 上図で、\(Z\)は最善の表現であるとすると、これは\(A\)から\(B\)への可能な写像を重なることなくすべてを含むような関数の集…

伊豆箱根鉄道駿豆線は東海道線の三島駅から伊豆市の修善寺までの19.8Kmを結び、車窓からは富士山を楽しむことができるローカル線だ。歴史的遺産が多く楽しむことができる。今回はこの路線の近くにある古い遺跡を訪れた。三島市の中心にあるのが伊豆国分寺で…