bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

恋人までの距離(Before Sunrise)-再会を期しての別れの場面

ジェシーセリーヌはウィーンの街へと繰り出す。かつてはハプスブルグ家がこの地に居城を開きヨーロッパの中心となっていた。さぞかし、有名な遺跡を巡るのかと思うとその期待は裏切られる。そう、二人にとっては観光旅行ではなく短いが楽しい時間そして愛をはぐくむときなのだから、会話だけがずっと続き景色は流れていく。
f:id:bitterharvest:20170802095741j:plain
プラーター公園で思い出に残る一晩を過ごした二人にも別れの時が来る。再びウィーン中央駅。エリーヌがパリへ向かう列車に乗り込む時二人は次の再会を約束する。
f:id:bitterharvest:20170802095022j:plain
いよいよ、別れの時が近づいてくる。二度と会わないと決めていたジェシーだが、それに耐えられなくなって切り出す。
“We're talking about not seeing each other again? I don't want that.”
「二度と会わないといっているけど、そんなの嫌だ」
セリーヌもそれに応じて、
“I don't want neither.”
「私もよ。」と言う。ジェシーは反復して、
“You don't neither?”
「あなたも。」と確認する。
“I waited for you to say it.”
「そう言ってくれるのを待っていたの。」とセリーヌが付け加える。
“Why didn't you say something?”
「なぜ言ってくれなかったの。」とジェシーがなじる。
“I was afraid you didn't wanna see me.”
「もしかして私に会いたくないではと考えてしまって聞けなかったの。」と微妙な心の動きを伝える。

そして、ジェシーは再会を約束するために切り出す。
“What do you wanna do?”
「それではどうしたい。」とジェシーは尋ねる。
“Maybe we should meet here in five years or something.”
「5年後ぐらいにここで会うのはどうかしら。」とセリーヌが提案する。ジェシーは即座に、
“Five years? That's a long time.”
「5年後。それは長すぎるよ。」と答える。
“it's awful. It's like a sociological experiment. How about one year?”
「そうよね。社会科学の実験みたいだわ。それでは1年後はどう。」と再提案する。
“One year. How about six months?”
「1年後。」ともう少し何とかならないかなあという姿勢をジェシーが示し、「6か月後では。」と新たな提案をする。
“Six months? It's gonna be freezing.”
「6か月後。凍てつくような寒さじゃない。」とセリーヌが躊躇する。
“Who cares? We come here, we go somewhere else.”
「誰がそんなこと気にするの。ここに来て、どこかに行けばいい。」
ジェシーが答えて次に会うことを約束する。さらに細かい時間や場所の取り決めをした後、会うときまではお互いに連絡を取り合わないことを約束して別れる。
別れの跡の画面が続く。その中の一つ。セリーヌが去った後の駅の様子を構外から見ているところ。
f:id:bitterharvest:20170802095241j:plain

さて、二人は6か月後に会えたであろうか。この続きは次作の『Before Sunset』で紹介されている。

恋人までの距離(Before Sunrise)-出会いの場面

専門分野の話は英語で話されても100%理解できる。しかし、映画となるとどうも心もとない。日常使うような言い回しを受験英語で学ぶことがほとんどなかったので戸惑いを感じるためだろう。

先日、カリフォルニアに住んでいるEdとGayeから、来年の秋にハワイのコンドミニアムで一緒に休暇を取らないかという誘いがきた。最近、英語を聞く機会がないので、力が落ちている可能性が高い。念のためにそれまでに耳を馴らしておいた方がよさそうだ。そこで、集中的に映画を観て準備することにした。ただ、観ただけでは面白くないので、その中で出てきた面白い表現を紹介することにしよう。

映画の説明に入る前に受験英語で失敗した例を最初に取り上げておこう。アメリカに留学し始めたころ、あるアメリカ人の家に泊まる機会があった。家に到着すると、両親はそのまま買い物に出かけてしまい、小学校低学年の子どもと彼の友達と一緒にいきなり留守番をさせられた。トイレの場所が分からなかったので子供たちに尋ねた。
“Where is the lavatory?”
そうしたら、予想もしないことが起こった。子供たちはいったん沈黙し、次の瞬間笑い転げながら部屋中を走り始めた。何とも古風な英語を東洋人から聞いてびっくりしたと同時におかしくなったのだろう。アメリカではbathroomが一般的だ(アメリカの家は浴室とトイレは一緒の部屋)。しかし受験英語ではこのようなことは教えてくれなかった。教科書として採用されるのは時代的には少し古い英語の小説(例えば、学校教育で英語を学ぶ最後となる大学2年の時はハーマン・メルヴィルの『白鯨』)がその頃はふつうであった。そこに出てくる単語を使ったので、「お主、厠はいずこにござ候。」ぐらいに聞いたのであろう。子供たちがびっくり仰天するのは当然のことであった。

最初に取り上げるのは、1995年作の『Before Sunrise (恋人までの距離)』である。偶然に車中で出会った男女が次の日の朝までのウィーンをぶらつきながら結びつき(connection)を強めていくという映画だ。

ジェシー(イーサン・ホークが演じる)はユーレイルパスを利用してブタペストからウィーンに向かっている。映画は流れていく線路を映し出した後ヨーロッパの美しい車窓を描き出す場面で始まる。
f:id:bitterharvest:20170731095650j:plain

ヨーロッパの6月は美しい。June Bride(6月に結婚式を挙げる花嫁)という言葉もあるぐらいで、人生の中で最も思い出に残るイベントをするべき時期と長いこと考えられてきた。この映画でも二人は6月16日に会っている。なだらかにうねっている薄緑色の丘陵地、それを囲むような深い緑の森、点在している白い壁の家々、そして青い空が織りなす風景がとてもきれいだ。

ソルボンヌ大学の女学生のセリーヌ(ジュリー・デルピー)は運悪く夫婦喧嘩をしているドイツ人夫婦とは通路を挟んで隣の席に座ってしまう。
f:id:bitterharvest:20170731112007j:plain
あまりの騒々しさに席を代え、ジェシーとは通路を挟んだ隣の席に移る。タイミングを計ってジェシーセリーヌに話しかける。とっつきに選んだのはもちろん夫婦喧嘩。二人とも何を話していたかは理解できなかったので、セリーヌが一般論に切り替える。
“Have you heard that as couples get older they lose their ability to hear each other?”
「夫婦は年を取ると相手が言っていることを聞く能力が失われるというのを聞いたことがある。」
セリーヌがもう少し詳しく説明した後で、ジェシーが次のようにまとめる。
“Nature's way of allowing couples to grow old together without killing each other, I guess.”
「夫婦がともに年を取ることができるように、そして連れ合いを殺さないで済むようにするための神からの恩恵だね。」
nature's wayの訳し方に工夫が必要だが、ここでは意訳した。

その後二人は、食堂車に移りコーヒーを飲みながら自己紹介をする。
f:id:bitterharvest:20170731112358j:plain
そうこうするうちに、ジェシーが下りるウィーンに到着する。彼は次の朝の飛行機でアメリカに帰ることになっているが、それまでの時間をセリーヌとともに過ごしたいと考えて、巧みにセリーヌを口説きにかかる。

列車から降りかけたジェシーは思いとどまり、セリーヌのところに再びやってくる。ヨーロッパの列車は大きな駅では長い時間停車している。日本でこんなことをしていると次の駅に連れていかれてしまうけれども、ヨーロッパでは十分に停車中の時間を楽しめる。また、ウィーンのような大きな駅は引き込み線になっている。丁度、日本の終着駅と同じで線路が行き止まりになっている。
f:id:bitterharvest:20170731112805j:plain
セリーヌの席にたどり着いたジェシーが次のように言う。
“I have an admittedly insane thought. If I don’t ask you this, it’ll haunt me the rest of my life.”
「自分でも非常識だと思うけど、このことを尋ねなければ、これからずっとこのことが頭から離れないと思うので、思い切って聞くけどいい。」
セリーヌが聞く。
“What?”
ジェシーが思いきって言う。
“I want to keep talking to you.”
「あなたと話し続けたい。」
“I have no idea what your situation is, but I feel like we have some kind of...connection.”
「あなたがどう思っているかは分からないけど、ある種の結びつき(connection)が僕たちにはあるように感じる。」
セリーヌも同じだという。「それでは、ウィーンで一緒に降りよう。僕は明日朝の飛行機に乗ることになっている。ただ、お金がなく、ホテルには泊まれないので、ウィーンの街を一緒に散策しよう。」と提案する。そして、極めつけの口説きに入る。
“Think of it like this.”
「このように考えてごらん。」
“Jump ahead, ten, twenty years, okay? And you're married.”
「10年後あるいは20年後の世界に飛び込んでみよう。そして、あなたは結婚している。」
“Only your marriage doesn't have that same energy that it used to have, you know. You start to blame your husband.”
「あなたの結婚には以前のような情熱はすでになく、ご主人を非難し始めている。」
“You start to think about all those guys you've met in your life, and what might have happened if you'd picked up with one of them?”
「これまでに会ったすべての男の人たちについて考え始めている。そのうちの一人をもし選んでいればどんなことが起こったのだろうかと考えている。」
“I'm one of those guys. That's me.”
「僕はそのうちの一人だ。そう僕だ。」
“So think of this as time travel from then to now to find out what you're missing out on.”
「これをタイムトラベルとして考えよう。未来から今への。あなたが若いころに逃したものを発見するための。」
“What this could be is a gigantic favor to both you and your future husband, to find out that you're not missing anything.”
「このことは素晴らしい贈り物だ。あなたとあなたの未来のご主人にとって。そして、あなたは何も逃していないことを発見する。」
“I'm just as big a loser as he is. Unmotivated. Boring.”
「僕は彼と同じでドジな男だ。やる気もないし、退屈な人間だ。」
ここは二人ともつまらない男だといっている。本来はご主人の方が優れていると言って良かったねというところなのだろうがそうではない。未来のご主人になれなかったジェシーが優れていたわけではないといっている。同程度にドジな男だといっている。どちらを選んでもよかったのだから、未来のご主人を選んだことに誤りはなかったと伝えたいのであろう。ご主人の方が優れていると言わなかったことで、ジェシーのプライドを示したかったのだろう。何となく引っかかる言回しなのだが、字幕の方は最初の文章は訳していない。単につまらない男だと伝えている。
“You made the right choice. You’re happy.”
「あなたは正しい選択をした。そして幸せだ。」

ジェシーの口説きは成功し、二人は列車を降りウィーンの街へと繰り出す。

映画の冒頭はドイツ語だった。列車がオーストリアを走行しているのでドイツ語で会話していることに違和感はないけれどもその他に理由はないのだろうか。国際列車なのでイタリア語でもよさそうだしフランス語でもよさそうだ。でもここは夫婦喧嘩の場面である。ヨーロッパで使われている主要な言語の中で、言い争っている場面に一番合いそうな言語は何と尋ねられればドイツ語と答えたい。力強く聞こえる言語で相手を説き伏せるには適しているように思える。

ウィーンはオーストリアの首都だ。標準語はもちろんドイツ語。歴史的な遺産がたくさん残されていて、旅行者から愛されている街だが、二人のconnectionはどのように展開していくのであろうか。それは次回の楽しみにということで今回はここまで。

若鶏のバスク風

鶏を丸ごと買ってきて作る料理を紹介しよう。頻繁に訪れる大型スーパーは周辺に外国人が多く住んでいるためかサイズの大きな肉が豊富に取り揃えられている。ステーキ用に300gサイズの豪州産牛肉が大量に並べられている。豚のステーキ肉も通常のものよりは2倍の厚みがある。そのような中で前から目をつけていたのが丸ごとの若鶏。一度購入しておいしい料理をと考えていた。

フランス料理の本をめくっていると、「若鶏のバスク風」というレシピに目が行った。バスクピレネー山脈の両麓に住んでいる人々を指す。西側がスペインに住むバスク人、東側がフランスに住むバスク人だ。彼らはバスク語を話す。今日のヨーロッパ言語とは親戚関係にない孤立した言語だ。彼らのY染色体はハプログループR1bが9割を占める。このハプログループの人々は新石器時代アナトリア(西アジア)からヨーロッパにわたり農耕を伝えたと考えられている(日本列島での弥生人と同じような役割を果たした)。かつてスペインのバスク地方の中心地ビルバオを訪問したことがある。とても良い印象を受けたこともありこの地方の料理を試みることにした。

今日の食材たちに登場してもらおう。
f:id:bitterharvest:20170718091329j:plain
主役はもちろん若鶏。脇役はトマト。味が淡白な若鶏をトマト味でスープに浸していただこうというものだ。トマト味に深みを持たせるのが、玉ねぎ(1個)、パプリカ(赤と黄のそれをそれぞれ半分)、ピーマン(3個)だ。パプリカは料理に彩を与える効果もある。肉の臭みはニンニクとブーケガルニだ。ブーケガルニは庭にあるハーブから作った。ローズマリー、セージ2種類、ラベンダー、レモンバームをただ束ねただけだ。

最初に取り掛かるのは若鶏をさばくことだ(丸ごと一羽で税抜き599円だった)。
f:id:bitterharvest:20170718092533j:plain
包丁でさばいてもよいのだが切れ味よく研いでないと肉が逃げるのでけがをする可能性が高い。簡単なのは調理用のはさみだ。レッグと手羽の部分はその付近の皮と腱を切り関節のところで折ると簡単に分離する。胸肉は骨に沿って肉を切り取ればよい、胸の骨はじょきじょきと簡単に切れるので適当な大きさに切ってだしとして用いればよい。切った後に塩・胡椒をする。
f:id:bitterharvest:20170718093405j:plain

玉ねぎ、パプリカ、ピーマンは1cm幅ぐらいに切る。
f:id:bitterharvest:20170718093751j:plain

大きなフライパンにオリーブオイル30ccを加えニンニクの細切りを加えてニンニクの焦げたにおいがするまで炒める。
f:id:bitterharvest:20170718094342j:plain
鶏肉を皮の方を下にしてフライパンに入れて焼き目が付いたころ裏返しにする。肉の側にも焼き目が付いたころ皿に移す。
f:id:bitterharvest:20170718094400j:plain

フライパンからニンニクを取り出し、オリーブオイルを20cc加えて玉ねぎ、パプリカ、ピーマンを加え、野菜類がしなやかになるまで炒める。そして、塩・胡椒をする。
f:id:bitterharvest:20170718094640j:plain

ホールトマト(1缶400g)をフライパンに加える。
f:id:bitterharvest:20170718095009j:plain

鶏肉をフライパンに戻し、ブールガリア、グリーンオリーブ、白ワイン(70cc)もフライパンに加える。
f:id:bitterharvest:20170718095153j:plain

弱火で15分間煮る。最後に塩・胡椒で味を調える。
f:id:bitterharvest:20170718095240j:plain

今日の主食とごはんとワインだ。
f:id:bitterharvest:20170718095359j:plain

孫がサッカーの試合を近くでしていたので夕食に加わった。お腹がすていたこともあるだろうが美味しい美味しいといって食べてくれた。

恩田川を散歩する

先日wowowで『4月の君の嘘』という映画を観た。高校生のラブストーリーだ。広瀬すずが扮するヴァイオリニストのかおりは余命いくばくもない。山崎賢人が演じる公生は天才的なピアニストととして幼いころは名をはせていたが、母親の死を境にしてピアノの音だけが演奏に集中すると聞こえなくなる。かおりは幼いころに公生の演奏を聴いて憧れる。いつか一緒に演奏をしたいという夢を抱き演奏を聴いた後ヴァイオリンを始めた。時が過ぎ、二人は同じ高校に入学する。かおりは公生に話す機会を得られないまま三年生になる。ある時、自分の余命が幾ばくも無いことを知り、思い切って公生に接近を図る。公生が再びピアノを演奏するように導いていくというラブストーリーだ。若者たちの付き合い方があっけらんかとしていて、受験勉強に明け暮れた我々の時代とはずいぶん違うなあと感じた。

しかし、それよりも驚かされたのは、日本の風景がきれいになったなあと思わせてくれたことだ。舞台は湘南、風景からすると鎌倉高校とその近辺のようだ。七里ガ浜、江の島、高校の周辺、公生の家の周辺がとても綺麗だ。かつてカリフォルニアに留学していた時にたびたび訪れたロスアンゼルス近郊のサンタ・モニカの景色にも負けないなと感じた。

気が付かなかっただけだろうと思うが今住んでいる住宅街も子供の頃になじんでいた風景とは大きく変わってとてもきれいになっている。ということで、住んでいる周辺の景色を写真で残しておこうと考えた。今日は、恩田川に沿って散歩をしたのでその風景からだ。この川は鶴見川の支流で横浜線に沿って流れている。小田急線と交わるあたりに源がある。家は町田市と横浜市の境にあるので、その日の気分によって東に下って横浜市側を歩いたり、西に上って町田市側を歩くことにしている。町田市側は桜並木が続き春先はとてもきれいである。この時期は渓谷を思わせる風景だ。
f:id:bitterharvest:20170717154815j:plain

横浜市側は水田や畑があり田園的な風景を醸し出している。夏は日差しが強く散歩には適していないが、今日は曇っていたので田園風景を楽しむために恩田川を下ってみた。田んぼの中を2両連結のこどもの国線の電車がのんびりと過ぎてゆく。
f:id:bitterharvest:20170717144047j:plain

道端には色々な草が咲いている。最近見つけたのがマツヨイグサだ。ツキミソウと間違って呼ばれることもあるが、本当のツキミソウは白い花だ。これに対してマツヨイグサの方は黄色である。
f:id:bitterharvest:20170717144548j:plain
f:id:bitterharvest:20170717145413j:plain

名前が分からないが、ピンク色のとてもかわいい花が咲いていた。
f:id:bitterharvest:20170717145528j:plain
マツヨイグサは家の庭にもこの5月まであった。草と思って間違って抜いてしまったために妻にえらく叱られ、それ以来散歩に出かけるたびにマツヨイグサを探していた。昨日初めて発見し道端の二本を抜いて持ち帰った。うまく育ってくれるとよいのだが。

恩田川に沿って横浜市市民農園がある。季節の野菜が所狭しと植えられている。中にはひまわりを植えている人もいる。
f:id:bitterharvest:20170717145125j:plain

路傍の花も綺麗だ。ツユクサはよく見かけるかわいい花だ。
f:id:bitterharvest:20170717145325j:plain

川には数日前に産まれたのだろう。まだ、泳ぎ方もぎこちない小さなカモの赤ちゃんが群れを成して移動していた。カラスに食べられずに育つといいなあと願って恩田川をあとにした。

伊東丸山公園で紫陽花を楽しむ(7月11日訪問)

地元の歴史研究会の秋の例会で縄文時代の家族システムについて説明することになっている。その準備作業をするために伊豆に逗留することが多くなってきた。インターネットも使えないような山の中で、小鳥の鳴き声を聞きながら緑の木立に囲まれリクライニングチェアを揺らしながら図書館から借りてきた書籍を読み漁っている。期待外れの本がないわけではないが、素晴らしいなと思わせてくれるものの方が多い。
最近読んだ本の中では、ジョナサン・ハイト(Jonathan Haidt)の「社会はなぜ左と右にわかれるのか――対立を超えるための道徳心理学(The Righteous Mind: Why Good People are Divided by Politics and Religion)」でその構想力の大きさに感嘆した。彼は、人間には生得的に与えられた6つのモラル基盤(Moral Foundations)があり、これらにより社会規範が作られていると主張している。どの社会規範が好きなのかはそれぞれの人のそれぞれのモラル基盤の強弱によるといっている。例えば、リベラルな人は6つのモラル基盤の中で「ケア」を大事にし、リバタリアンと呼ばれる人は「自由」を大切にすると説明している。
f:id:bitterharvest:20170717084344j:plain

ハイトのモラル基盤とエマニュエル・トッドの家族システムを利用して、縄文時代の社会がどのようになっていたかを読み解こうともがいているときに、内容は忘れてしまったが何とも薄気味悪い夢を見て真夜中にもかかわらず目覚めてしまった。重い気分の中で何となく耳に違和感を覚えたのもつかの間、奥の方で激しい痛みを感じた。東京に戻ることは難しそうなので、地元の耳鼻科にかかろうということで痛みに耐えながら夜が明けるのを待って、最も近い耳鼻科といっても逗留している場所から20kmも離れている病院に駆け込んだ。

中耳炎になっていると説明を受け、鼓膜を切開した方が直りが早いといわれ、「お願いします」と答えてしまった。麻酔をするから痛くないだろうとたかをくくったのがいけなかった。麻酔液を点耳して10分間待つ。これで終わりだ。外科や歯医者と違って麻酔が効いているかどうかを確認しない。麻酔が効いてないのではという嫌な予感がする。ちょっと我慢してといわれて長い針のようなものを刺される。「ギャ」と言いたいところなのだが歯を食いしばって耐える。その後、膿を吸い出してもらう。最後に、チューブを入れますといわれた。これは予想していなかったことだが、これから耳だれがたくさん出てくるので、それを通すための管ということだった。この挿入もまた痛い。しかし、これで耳の激しい痛みも治まれば報われると前向きに考えて、素直に治療を受けた。

その後、通院を続けている。珍しく妻が伊豆に滞在したときに、少し時期遅れになったが紫陽花の綺麗な場所を探して梅雨時の一日を楽しむこととした。伊東の近くの丸山公園はまだ大丈夫だという情報を得てそこを訪れることにした。

丸山公園は伊東駅から歩いても20分くらいのところにある。伊東の市街地は伊豆急行線の海側の方に開けているが、丸山公園は山側の方にある。携帯のナビを使っていつ着くのかと不安になりながら小沢川沿いの細い坂道を登って行く。住宅街が切れたころ公園の入り口にようやくたどり着いた。
f:id:bitterharvest:20170717093504j:plain

丸山公園は大平の森ハイキングコースの入り口にもなっている。
f:id:bitterharvest:20170717093644j:plain

公園の入り口から少し入るとそこは渓谷の世界である。
f:id:bitterharvest:20170717093824j:plain

沢に沿って紫陽花が植えられている。
f:id:bitterharvest:20170717093943j:plain
f:id:bitterharvest:20170717094017j:plain

ハイキングコースに沿っても綺麗に咲いている。
f:id:bitterharvest:20170717094151j:plain
f:id:bitterharvest:20170717094334j:plain

山百合も負けじと咲いていた。
f:id:bitterharvest:20170717094247j:plain

水辺にも橙色の花(ヒメオウギズイセン)が咲いていた。
f:id:bitterharvest:20170717094712j:plain

丸山公園は梅や桜や紅葉の名所でもあり蛍も飛び交う場所なので、来年もまた訪れて見ようと決意して来た道を引き返した。

関手圏

9.関手圏

9.1 小さな圏の圏

圏は、対象と射で構成されていた。そこで、対象を圏とし、射を関手とする圏を考えることができる。しかし、この圏を作るにあたっては少し制約を設けている。これは圏から圏を作るということになるので、集合の集合を考えるときと同じような問題が生じる。

集合の集合にはいわゆるラッセルのパラソックスと呼ばれえるものがある。集合の集合は集合にはならないというパラドックスである(開集合を定義するときに、有限個の開集合の論理積は開集合と定義しているのを思い出してほしい。無限個の開集合の論理和は開集合と定義しているが、無限個の開集合の論理積については定義していない。これはラッセルのパラドックスを避けるための工夫である。無限個の開集合の論理積を許すとどのような矛盾が生じるかを考えると分かるので試みて欲しい)。

このパラドックスが生じないようにするために、圏から圏を構成するためには、小さな圏を用いて圏を構成するという制約を設ける。

小さな圏とは、それを構成する対象も射も集合であるという制約である(そうでないときは大きな圏という)。この制約を用いれば、関手を用いて圏から圏を構成することができる(大きな圏から作られた圏とならない場合がある)。

小さな圏の圏は\(\rm{Cat}\)で表す。

9.2 関手圏

関手を対象とし、自然変換を射とする圏を作成することを考える。

1) 二つの圏から関手圏を作成する

小さな圏を\(\mathcal{C,D}\)をした時、この小さな圏の間の関手を対象とし、関手のコドメイン間の自然変換を射とした圏は関手圏と呼ばれ、\([\mathcal{C},\mathcal{D}]\)あるいは\(\mathcal{D}^\mathcal{C}\)と表される。

それでは、一般的な関手圏を構成してみよう。次の手順に従って作成していく。

1) 対象を小さな圏\(\mathcal{C},\mathcal{D}\)間の関手\(F,G,H,...\)としよう。
2) 射を\(F\)から\(G\)への自然変換\(\alpha\)、\(G\)から\(H\)への自然変換\(\beta\)、\(F\)から\(H\)への自然変換\(\gamma\),...としよう。
3)自然変換のドメインとコドメインはその成分ごとのドメインとコドメインとなるようにしよう。これは次のようになる。\(\alpha\)の成分\(\alpha_A:F(A) \rightarrow G(A)\)とする。\(F\)のドメインは\(A\)である。これのコドメインを\(A'_F\)とする。この時、\(F:A \rightarrow A'_F\)であり、\(F\)のイメージ\(F(A)\)は\(F(A) \subset A'_F\)となる。同様に、\(G\)に対してもコドメイン\(A_G\)が存在する。そして、厳密に\(\alpha_A\)を定義すると\(\alpha_A:A'_F \rightarrow A'_G\)であるが、本質は失われないので、便宜的に\(\alpha_A:F(A) \rightarrow G(A)\)と書くことにする。
4) 恒等射は同じ関手間での自然変換としよう。例えば、関手\(F\)に対する恒等射を\(id_F\)とする。この成分を\(id_A\)とすると、\(id_A : F(A) \rightarrow F(A)\)となる。即ち、\(F:A'_F \rightarrow A'_F\)であり、\(F(x \in A'_F) = x\)である。
5) 自然変換の合成を成分での合成にしよう。例えば、\(\gamma=\alpha \circ \beta\)を次のように成分ごとに定義する。即ち、\(\gamma_A=\alpha_A \circ \beta_A\)とする。

言葉ではわかりにくいので、図で示すことにしよう。対象\(F,G\)と射\(\alpha\)の成分\(\alpha_A\)を示したのが下図である。1)で構成した対象は関手\(F,G\)であり、2)で構成した射は自然変換\(\alpha\)であり、その成分は\(\alpha_A\)である。
f:id:bitterharvest:20170609214635p:plain
この図で次のことに注意してほしい。\(F(A)\)は関手のイメージであり、関手のコドメイン\(A'_F\)は\(F(A) \subset A'_F\)である。同様に、関手\(G\)のコドメイン\(A'_G\)とすると、自然変換\(\alpha\)の成分\(\alpha_A\)は\(\alpha_A : A'_F \rightarrow A'_G\)である。

5)の射の合成は下図のようになる。図では、自然変換\(\alpha\),\(\beta\)の合成が自然変換\(\gamma\)となる様子を示したものである。即ち、それぞれの成分\(\alpha_A\),\(\beta_A\)の合成が\(\gamma\)の成分\(\gamma_A\)となる。
f:id:bitterharvest:20170609222131p:plain

さらに、圏\(\mathcal{C}\)の対象\(A\)が射\(f\)によって対象\(B\)によって写像されるときの、自然変換の関係を示したのが下図である。ここで、\(\alpha_A\)と\(\alpha_B\)は、自然変換\(\alpha\)の成分である。即ち、\(\alpha_A\)はドメインを\(A\)とした成分で、\(\alpha_B\)はドメインを\(B\)とした成分である。\(\beta\),\(\gamma\)についても同様である。
f:id:bitterharvest:20170609222547p:plain
上記の図は可換図式となっていることに注意してほしい。即ち
\begin{eqnarray}
\alpha_B \circ F(f) &=& G(f) \circ \alpha_A \\
\beta_B \circ G(f) &=& H(f) \circ \beta_A \\
\gamma_B \circ F(f)=\beta_B \circ \alpha_B \circ F(f) &=& H(f) \circ \beta_A \circ \alpha_A = H(f) \circ \gamma_A
\end{eqnarray}

また、4)の恒等射を示したのが下図である。
f:id:bitterharvest:20170609222822p:plain

上記の手順によって構成したものが圏となるためには、単位律と結合律を満足しなければならない。

単位律は成分ごとに\(id_A \circ \alpha_A = \alpha_A = \alpha_A id_A\)を示せばよい。なお、前者の\(id_A\)は\(id_A: G(A) \rightarrow G(A)\)であり、 後者の\(id_A\)は\(id_A: F(A) \rightarrow F(A)\)である。

結合律は、自然変換\(\alpha,\beta,\gamma\)が与えられた時、\((\alpha \circ \beta) \circ \gamma=\alpha \circ (\beta \circ \gamma)\)が成り立つことを示せばよい。これは、成分ごとに、即ち、\((\alpha_A \circ \beta_A) \circ \gamma_A=\alpha_A \circ (\beta_A \circ \gamma_A)\)が成り立つことを示せばよい。

2) 関手圏の小さな圏の圏の一員

関手圏は、小さな圏から構成された圏(先の例では\(\mathcal{C,D}\)から構成された圏)と見なすことができるので、小さな圏の圏\(\rm{Cat}\)の一員である。
f:id:bitterharvest:20170610114515p:plain

この圏では、図に示すように、関手を1-cellと呼び、自然変換を2-cellと呼ぶ。また、圏は0-cellと呼ばれる。自然変換を2-cellを射とした圏を2-圏(2-category)という。また、関手圏を小さな圏の対象とすることもできる。これにより、高次の圏を構成できる。

3) 三つの圏から関手圏を作成する

先の例では、二つの圏から関手圏を構成したが、今度は三つの圏から関手圏を構成することを考える。言葉で示すよりも図で示したほうが分かりやすいので、そのようにする。
f:id:bitterharvest:20170610104754p:plain



圏\(\mathcal{C}\)から圏\(\mathcal{D}\)への関手を\(F,F'\)とする。また、\(F\)から\(F'\)への自然変換を\(\alpha\)とする。同様に、圏\(\mathcal{D}\)から圏\(\mathcal{E}\)への関手を\(G,G'\)とし、\(G\)から\(G'\)への自然変換を\(\beta\)とする。この時、対象を\(F,F',G,G'\)とし、射を\(\alpha,\beta\)とした関手圏が上手に示すものである。

また、\(\mathcal{C}\)で対象\(A\)から\(B\)への射を\(f\)とした時、下図のような可換図式を得ることができる。
f:id:bitterharvest:20170610112132p:plain
自然変換としての条件がどのように満たされているかは、とても煩雑な作業だが、読者の方で確認して欲しい。

9.3 圏論をさらに探求すると

以下では、圏論をさらに進めるとどのような世界が開けてくるのかについて簡単に説明する。

1) Bicategory

Bicategoryは2-圏(2-category)の条件を緩めたものである。2-圏では、単位律と結合律が成り立つことを必要条件としていたが、これを同型写像でよいとしたものである。即ち、単位元については、\(id \circ \alpha\)と\(\alpha \circ id\)の間に同型写像が存在すればよいとしたものである。結合律についても、\((\alpha \circ \alpha) \circ \gamma\)と\(\alpha \circ (\alpha \circ \gamma)\)の間に同型写像が存在すればよいとしたものである。

2) Homotopy Type Theory

圏では、射は一方向であった。射が両方向であることを条件に圏と同じような構造を構造を立てることができる。これは圏に代わってGroupoidと呼ばれる。2-categoryを定義したときと同じようにGroupoidの上に高次のGroupoidを構成することができる。高次が無限のレベルになるとHomotopy Type Theoryと呼ばれるものになる。

シュークルート:アルザス地方のキャベツの漬物とバーコン・ソーセージの煮込み料理

ザワークラウトが半分ほど残っていたので、これを使ったおいしそうな料理をということでシュークルートを作ることにした。

ザワークラウト(Sauerkraut)はドイツ語でキャベツの漬物である。もともとの意味は酸っぱいキャベツだ。この酸っぱさは、酢からではなく乳酸発酵によるものだ。ドイツだけではなく、フランスのアルザス地方や北欧、東欧でも食されている。今回は、ザワークラウトを用いてアルザス地方の家庭料理であるシュークルート(Choucroute)を作ってみよう。

料理の名前はフランス語だが、主たる食材のザワークラウトはドイツ語だ。何となく複雑な歴史を感じさせるが、アルザス地方はドイツ領になったりフランス領になったりと幾たびかの戦争に翻弄されてきた地方だ。

シュークルートは、ベーコンやソーセージなどの肉類を野菜とともに、ザワークラウトの味をベースにして、白ワインで煮込む料理だ。本当は、アルザス地方のリースリングで味付けするといいのだが、今回は、オーストラリア産のシャルドネで料理することにした。今日の食材に登場してもらおう。
f:id:bitterharvest:20170608214712j:plain

肉類と野菜を料理しやすいように、皿に盛っておく。野菜の方は、玉ねぎ(半分)を薄切りに、ジャガイモ(2個)とにんじん(1本)は乱切りにし、下ゆでする。
f:id:bitterharvest:20170608215254j:plain
フライパンにバターを入れて、肉類の表面に焦げ目が入る程度に焼いておく。最初はベーコン(150g)、
f:id:bitterharvest:20170608215526j:plain
次は豚のバラ肉(150g)、
f:id:bitterharvest:20170608215644j:plain
最後は白ソーセージ(9本)だ。
f:id:bitterharvest:20170608215728j:plain
フライパンに残っている肉からでた油をそのまま用いて、ニンニク(2かけ)と玉ねぎ(半個)を玉ねぎがしんなりするまで炒める。
f:id:bitterharvest:20170608220518j:plain
ザワークラウト(170g)をフライパンに加える。
f:id:bitterharvest:20170608220656j:plain
ベーコンと豚バラ肉を加える。
f:id:bitterharvest:20170608220803j:plain
さらに、ソーセージを加える。
f:id:bitterharvest:20170608220837j:plain
ジャガイモ、ニンジンを加える。
f:id:bitterharvest:20170608221104j:plain
最後に白ワイン(1/3本)を加えるとともに水(100CC)を加える。
f:id:bitterharvest:20170608221127j:plain
マギーブイヨンを加え、沸騰させた後で、40分間弱火で煮詰める。

シュークルートが出来上がるまで、バーニャカウダ(Bagna càuda)と白ワインを楽しむ。
f:id:bitterharvest:20170608221442j:plain

白ワインがなくなってきたころ、シュークルートが出来上がった。
f:id:bitterharvest:20170608221615j:plain
皿に盛るとこのようになる。
f:id:bitterharvest:20170608221722j:plain
これにイタリアンパセリをのせ、マスタードをつけるはずであったが、白ワインがあまりにもおいしかったので、忘れてしまった。しかし、ザワークラウトの酸味が程よくきいていて、アルザス地方のおいしい料理を楽しんだ、

自然変換

8. 自然変換

圏論の話もそろそろ終わりに近づいてきた。これまでの話の中で重要であった話題は、圏そのものと、関手である。圏は計算の構造を示し、関手は構造を維持しての圏から圏への射を与えてくれる。今回は、この二つの概念に劣らないほどに重要な自然変換(natural transformation)の話をする。

8.1 自然変換の定義

自然変換は関手のイメージ間での射を定めるものである。今二つの圏\(\mathcal {C,D}\)を考えよう。二つの関手\(F,G\)が与えられたとする。図に示すように、\(F(A)\)は、\(F\)によって\(\mathcal {C}\)の対象\(A\)を写像した時のイメージとする。同様に、\(G(A)\)は\(G\)によるイメージとする。
f:id:bitterharvest:20170606092255p:plain

\(F(A)\)から\(F(B)\)への射を\(\alpha_A\)とする。

また、\(f\)は\(\mathcal {C}\)で\(A\)を対象\(B\)に移す射とする。この時、\(B\)は\(F\)により\(F(B)\)に、\(G\)により\(G(B)\)に移される。また、\(f\)は\(F\)により\(F(f)\)に、\(G\)により\(G(f)\)に移される。図で示すと以下のようになる。
f:id:bitterharvest:20170606092318p:plain

この時、圏\(\mathcal{D}\)の中に生じている\(F(A)\)から\(G(B)\)に至る四角形のグラフが、全ての\(A\)に対して可換(すなわち、\(\alpha_B \circ F(f) = G(f) \circ \alpha_A\)になっているとき、すぐ後に定義するが、自然変換であるという。

可換図式のところをもう少し詳しく示すと以下のようになる。対象\(A\)内の要素\(x\)は図に示すように移される。
f:id:bitterharvest:20170606092331p:plain
なお、上の図で、\(F(B)\)はある対象の内部になることもあるので、\(\alpha_B\)は一意に定まらないことに注意してほしい。

それでは、自然変換についての定義をしておこう。
\(F,G\)が、二つの圏\(\mathcal{C,D}\)の間の関手であって、次の二つの条件1),2)を満たす時、\(F\)から\(G\)への自然変換\(\alpha\)は射(morphisms)の族(family)である。
1) 自然変換は、\(\mathcal{C}\)の全ての対象Aに対して、\(\mathcal{D}\)のある対象(複数の場合もある)に関連づける射\(\alpha_A\)が存在する。\(\alpha_A\)は\(A\)での\(\alpha\)の成分(Component)という。
2)全ての成分は\(\mathcal{C}\)の全ての射\(f:A \rightarrow B\)に対して、\(\alpha_B \circ F(f) = G(f) \circ \alpha_A\)でなくてはならない。

8.2 ポリモーフィズム

Haskellのプログラムでは、自然変換はポリモーフィズム(polymorphism)を用いて記述される。ポリモーフィズムは日本語では多態性、多相性、多様性などと呼ばれるが、ここではポリモーフィズムと表すことにする。ポリモーフィズムプログラミング言語の型システムの性質を表すもので、プログラミング言語の各要素についてそれらが複数の型に属することを許す。Haskellでは、型変数を用いてポリモーフィズムは実現される。また、Haskellでは、自然変換の条件は自然に満たされるので、プログラミングするときに気を使う必要はない。

alpha :: F a -> G a
alpha . (fmap f) = (fmap f) . alpha

上記の定義で、\( alpha :: F \ a \rightarrow G \ a\)は\( alpha :: forall \ a . F \ a \rightarrow G \ a\)を表しているので、全ての型\(a\)に対して成り立つという意味である。即ち、図中の\(F(A) \rightarrow G(A)\)に対しても\(F(B) \rightarrow G(B)\)に対しても成り立つ(これにより、自然変換の条件1)は満足される)。
例を示そう。
リストの先頭を安全に出力する関数\(safeHead\)を定義しよう。\(safeHead\)を定義するためには、\(F\)をリストにする関手\([ ]\)に、\(G\)を関手\(Maybe\)として実現すればよいので下図のようになる。
f:id:bitterharvest:20170606092400p:plain
それでは、\(safeHead\)を定義してみよう。

safeHead :: [a] -> Maybe a
safeHead [] = Nothing
safeHead (x:xs) = Just x

それでは、自然変換の条件2)の\(\alpha_B \circ F(f) = g(f) \circ \alpha_A\)が満たされていることを確認しよう。まず、

safeHead [] = Nothing

について考える。この場合、以下が満たされることを示せばよい。

safeHead . ( fmap f) $ [ ] = fmap f $ Nothing

右辺の方は次のようになる。

safeHead . ( fmap f) $ [ ]
= safeHead $ fmap f [ ]
= safehead [ ]
= Nothing

左辺は次のようになる。

fmap f $ Nothing
= Nothing

従って、両辺は同じである。

safeHead (x:xs) = Just x

についても確認しよう。
この時は、以下が満たされることを示せばよい。

safeHead . (fmap f) $ (x:xs) = (fmap f) . safeHead $ (x:xs) 

右辺は

safeHead . (fmap f) $ (x:xs) 
= safeHead $ fmap f (x:xs) 
= safehead $ (f x: fmap f xs) 
= Just (f x)

左辺は

(fmap f) . safeHead $ (x:xs) 
= fmap f $ safeHead (x:xs) 
= fmap f $ Just x 
= Just (f x)

同じように、両辺は一致する。従って、自然変換の条件2)は満たされていることが分かる。

ついでに、この関数を利用して確認してみよう。\(f\)を\(length\)とした場合である。

*Main> safeHead . (fmap length) $ ["better", "bad", "ok"]
Just 6
*Main> (fmap length) . safeHead $ ["better", "bad", "ok"]
Just 6

\(f\)を\((+2)\)とした場合である。

*Main> safeHead . (fmap (+2)) $ [1,2,3,4]
Just 3
*Main> (fmap (+2)) . safeHead $ [1,2,3,4]
Just 3

別の例を示そう。関手が二つあって、\(Identity\)は自分自身に\([ ]\)はリストに移すものとする。図で示すと以下のようになる。

また、\(Identity \ a\)をリスト\([a ]\)に変換する関数を\(toList\)としよう。
f:id:bitterharvest:20170606092418p:plain

プログラムで表現すると以下のようになる。

data Identity a = Identity a deriving (Show, Read, Eq)

instance Functor Identity where
  fmap f (Identity a) = Identity (f a)

toList :: Identity a -> [a]
toList (Identity a) = [a]

下記が成り立っていることをプログラムで確認してみよう。

alpha :: F a -> G a
alpha . (fmap f) = (fmap f) . alpha

\(f\)に\((+3)\)と\(length\)を利用してみよう。

*Main> fmap (+3) (Identity 4)
Identity 7
*Main> Identity ((+3) 4)
Identity 7
*Main> fmap length (Identity "Tom")
Identity 3
*Main> Identity (length "Tom")
Identity 3

実行結果から右辺と左辺が一致していることが分かる。時間がある人は、一般的に\(f\)についても成り立つことを証明してほしい。

サーモンと玉ねぎ・ピーマンのクリーム煮

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

でも、良いことばかりではなさそうだ。だんだん慣れてくるに従って、オーブン料理を敬遠するようになってきた。オーブン料理を作るときは、一つしかないスチームオーブンレンジを用いるが、このオーブンレンジは調理前も後も他の目的のために使うことができない。調理前は余熱のためなので我慢できるが、調理後の庫内の熱を冷ます時は面食らう場合が多い。オーブン料理ができた後で、レンジで温めたいと思うことが少なからずあるためだ。それも悪いことに、オーブン料理が出来上がるころに思いつくので始末に悪い。

スチームオーブンレンジの欠点を補ってくれるのがオーブントースターだ。庫内を温める必要もないし、冷ます必要もない。今回は、オーブントースターを用いて、新しい道具の利用法を開拓することにした。

デパ地下の食料品売り場で新鮮な生鮭を見つけた(2切れ購入し、等分に切った)。
f:id:bitterharvest:20170521094518j:plain
これを利用して「サーモンと玉ねぎ・ピーマンのクリーム煮」を作ることにした。サーモンと玉ねぎだけで作れるので、いたって簡単な料理である。今回は、ピーマンも加えたが、これは衝動的である。生鮭を手にした後に寄った野菜売り場で、ピーマンの安売りをしていた。一袋300円となっていたが、売り子のおばさんが袋に一杯詰めた後で、さらに5個付け加えた。袋からは完全にあふれていたが、これも一袋だからということで、甘い言葉に乗って、買ってしまった。あまりにも、たくさんのピーマンを手にしたので、これも用いることにした。

グラタン皿を二つ用意して、それぞれに。オリーブ油を小さじ1杯たらした。玉ねぎ1/4個を細切りにして、それをグラタン皿の底に敷いた。
f:id:bitterharvest:20170521094607j:plain
さらに、ピーマン1個を切って、グラタン皿に加えた。
f:id:bitterharvest:20170521094911j:plain
塩(それぞれに一つまみ)と胡椒(2,3振り)を振りかけた生鮭をグラタン皿に加えた。
f:id:bitterharvest:20170521095250j:plain
生クリーム(50mg)とサワークリーム(大匙3杯)を別の器でかき混ぜ、これに、塩、胡椒を加える。
f:id:bitterharvest:20170521095509j:plain
かき混ぜた生クリームとサワークリームを生鮭の上に加える。
f:id:bitterharvest:20170521095624j:plain
オーブントースターで12分間焼く。
f:id:bitterharvest:20170521095722j:plain
ディルを上にまぶす。
f:id:bitterharvest:20170521095814j:plain
さらに、レモンを加えて食卓に供する。
f:id:bitterharvest:20170521095927j:plain
魚臭さもなく、クリーム味を楽しむことができ、期待通り、コスト・パーフォーマンスのよい料理であった。

写像対象-カリー=ハワード同型対応

7.9 カリー=ハワード同型対応

世の中には、言い方は違っているのだが、同じことを言っているということが往々にしてある。

前回の記事で、型定理と圏論は一対一に対応づけできると説明したが、その例の一つである。さらに、もう一つ対応するものがある。それは、型定理と論理だ。

論理、型定理、圏論の関係を示すと以下のようになる。

意味 論理 型定理 圏論
真(true) \(True\) \(()\) (ユニット) 終対象
偽(false) \(False\) \(Void\) 始対象
論理積(conjunction) \(A \land B\) \((a,b)\) (デカルト積) \(A \times B\) (直積)
論理和(disjunction) \(A \lor B\) \(Either \ a \ b\) \(A + B\) (余積)
含意(implication) \(A \rightarrow B\) \(a \rightarrow b\) (関数型) \(B^A\) (指数対象)
含意除去(modus ponens) \((A \rightarrow B \land A) = B\) \((a \rightarrow b,a) = b\) \((B^A \times A) = B\)

この関係が成り立つので、プログラムの証明が可能になるが、それについてはいずれかの機会にしたいと思う。ここでは、論理、型定理、圏論の関係を示すに止めておき、次回は、自然変換(natural transformation)の話題に移行する。

注:\(a \rightarrow b\)はこれまでは説明しなかった。これは、すでに説明した写像対象\(A \rightarrow B\)を型に変えたものである。そして、関数の形をとっているので、関数型と呼ばれる。

写像対象-型定理(続き)

7.8 具体例

指数対象\(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}
となることを前回の記事で説明した。

それでは、この型シグネチャに基づいて具体例を提示することにしよう。

対象\(A,B,C\)をそれぞれ2個の文字の集まり\(\{A,B\}\)、3個の整数の集まり\(\{1,2,3\}\)、ブール値\(\{True,False\}\)としよう。

まず、左辺の
\begin{eqnarray}
Either \ b \ c \rightarrow a
\end{eqnarray}
を実現しよう。これは、\(A\)か\(B\)を入力し、\(C\)を出力する射の集まりを求めているので、次の32個の関数として実現することができる。

f1 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f2 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f3 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f4 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f5 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f6 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f7 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f8 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f9 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f10 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f11 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f12 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f13 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f14 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f15 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f16 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f17 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f18 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f19 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f20 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f21 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f22 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f23 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f24 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f25 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f26 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f27 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f28 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f29 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f30 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f31 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f32 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"

次に、右辺の
\begin{eqnarray}
(b \rightarrow a, c \rightarrow a)
\end{eqnarray}
を実現しよう。

まず、\(b \rightarrow a\)を実現しよう。これは次のようになる。

g1 a
  | a == 'A' = True
  | a == 'B' = True
  | otherwise = error "not assigned"
g2 a
  | a == 'A' = True
  | a == 'B' = False
  | otherwise = error "not assigned"
g3 a
  | a == 'A' = False
  | a == 'B' = True
  | otherwise = error "not assigned"
g4 a
  | a == 'A' = False
  | a == 'B' = False
  | otherwise = error "not assigned"

同様に、\(c \rightarrow a\)を実現すると、次のようになる。

h1 a
  | a == 1 = True
  | a == 2 = True
  | a == 3 = True
  | otherwise = error "not assigned"
h2 a
  | a == 1 = True
  | a == 2 = True
  | a == 3 = False
  | otherwise = error "not assigned"
h3 a
  | a == 1 = True
  | a == 2 = False
  | a == 3 = True
  | otherwise = error "not assigned"
h4 a
  | a == 1 = True
  | a == 2 = False
  | a == 3 = False
  | otherwise = error "not assigned"
h5 a
  | a == 1 = False
  | a == 2 = True
  | a == 3 = True
  | otherwise = error "not assigned"
h6 a
  | a == 1 = False
  | a == 2 = True
  | a == 3 = False
  | otherwise = error "not assigned"
h7 a
  | a == 1 = False
  | a == 2 = False
  | a == 3 = True
  | otherwise = error "not assigned"
h8 a
  | a == 1 = False
  | a == 2 = False
  | a == 3 = False
  | otherwise = error "not assigned"

右辺はこれらのデカルト積となるので、次の32個の関数として実現される。

p1 a b  = ((g1 a), (h1 b)) 
p2 a b  = ((g1 a), (h2 b)) 
p3 a b  = ((g1 a), (h3 b)) 
p4 a b  = ((g1 a), (h4 b)) 
p5 a b  = ((g1 a), (h5 b)) 
p6 a b  = ((g1 a), (h6 b)) 
p7 a b  = ((g1 a), (h7 b)) 
p8 a b  = ((g1 a), (h8 b)) 
p9 a b  = ((g2 a), (h1 b)) 
p10 a b = ((g2 a), (h2 b)) 
p11 a b = ((g2 a), (h3 b)) 
p12 a b = ((g2 a), (h4 b)) 
p13 a b = ((g2 a), (h5 b)) 
p14 a b = ((g2 a), (h6 b)) 
p15 a b = ((g2 a), (h7 b)) 
p16 a b = ((g2 a), (h8 b)) 
p17 a b = ((g3 a), (h1 b)) 
p18 a b = ((g3 a), (h2 b)) 
p19 a b = ((g3 a), (h3 b)) 
p20 a b = ((g3 a), (h4 b)) 
p21 a b = ((g3 a), (h5 b)) 
p22 a b = ((g3 a), (h6 b)) 
p23 a b = ((g3 a), (h7 b)) 
p24 a b = ((g3 a), (h8 b)) 
p25 a b = ((g4 a), (h1 b)) 
p26 a b = ((g4 a), (h2 b)) 
p27 a b = ((g4 a), (h3 b)) 
p28 a b = ((g4 a), (h4 b)) 
p29 a b = ((g4 a), (h5 b)) 
p30 a b = ((g4 a), (h6 b)) 
p31 a b = ((g4 a), (h7 b)) 
p32 a b = ((g4 a), (h8 b)) 

このように、左辺、右辺ともに32個の関数で実現され、これらの関数は1対1に対応させることができ、同型写像(Isomorphism)であることが分かる。

少しだけ、実行してみよう。

*Main> f27 (Left 'A')
False
*Main> f27 (Right 1)
True
*Main> p27 'A' 1
(False,True)

写像対象-型定理

7.7 型定理(Type Theory)

型定理という言葉に戸惑う人も多いことと思う。日本語版のウィキペディア型理論を検索するとあまりにも短い記述にがっかりするだろう。得られる情報も余りない。しかし、さすがに英語版の方には詳しく書いてある。その記述の中に、圏論との関係についての記述がある。その中で、ジョン・ベル(John Lane Bell)が「圏は、ある種の型定理と見なすことができる」と書いていると紹介されている。その紹介に続いて、対象を型に変更すれば、圏は型定理になるとも書かれている。

対象を型に変えるという表現はどこかで見たような気がしないだろうか。そう、圏論Haskellに変えるときに使っていた表現だ。なんてことはない。圏論の定理を型定理で解釈したほうが分かりやすい場合があることも経験的にわかっている。そこで、今回は、指数対象で成り立っている定理のいくつかについて、型定理での解釈を試みよう。

例を説明する前にこれまでの復習をしておこう。

\(A \Rightarrow B\)は、ドメイン\(A\)からコドメイン\(B\)への余すところのない、また、重複することのない射の集まり(集合)であった。そして、射の集まりは圏論では対象と見なすことができるので、これに特別な名前を与えて、写像対象と呼んだ。

\(A\)が\(m\)個の要素、\(B\)が\(n\)個の要素から成り立っているとき、射の総数は\(n^m\)である。

射の総数の表し方に似せて、写像対象\(A \Rightarrow B\)を\(B^A\)と書くことにする。\(B^A\)は指数対象と呼ばれる。指数対象が射の集まりであることに注意すると、二つの指数対象\(B^A\)と\(D^C\)が与えられた時、それぞれを構成している射の総数が同じである時、二つの指数対象には1対1の関係が成り立つ。この時、二つの指数対象は同型写像(Isomorphism)が成り立つという意味において同値であるといい、\(B^A = D^C\)と記述することとする。

また、Haskellでは対象は型(タイプ)として表される。指数対象\(B^A\)は型となるが、\(A\)も\(B\)も共に型である。Haskellでは型は小文字で記述されるので、\(a\),\(b\)と記述される。これは型変数とも呼ばれる。指数対象は射の集まりなので、Haskellでは型シグネチャで記述され、\(B^A\)は\(a \rightarrow b\)となる。

二つの指数対象\(B^A\)と\(D^C\)が同値の時、それぞれの型シグネチャは1対1に対応するので、
\begin{eqnarray}
a \rightarrow b \sim c \rightarrow d
\end{eqnarray}
と記述することにする。

それでは例を示すことにしよう。

1) \(A^{B+C}=A^B \times A^C\)

圏論では\(A^{B+C}=A^B \times A^C\)が成り立つ。これを、型定理、即ち、Haskellで解釈してみよう。

\(B+C\)は型定理では\(Either \ b \ c\)である。左辺\(A^{B+C}\)は\(B+C\)を入力とし\(A\)を出力とする射の集まりなので、型定理では\(Either \ b \ c \rightarrow a\)となる。

\(A\)と\(B\)のデカルト積、即ち、\(A \times B\)は型定理では\((a,b)\)である。右辺\(A^B \times A^C\)は二つの射の集まり\(A^B\)と\(A^C\)のデカルト積なので、型定理では\((b \rightarrow a, c \rightarrow a)\)となる。

従って、\(A^{B+C}=(A^B \times A^C)\)は型定理では
\begin{eqnarray}
Either \ b \ c \rightarrow a \sim (b \rightarrow a, c \rightarrow a)
\end{eqnarray}
といっている。

2) \(A^{B^C}=A^{B \times C}\)

左辺\(A^{B^C}\)は、\(C\)という入力から、(\(B\)を入力とし\(A\)を出力とする)射を出力とするような射の集まりなので、型定理では\(c \rightarrow (b \rightarrow a)\)となる。

右辺\(A^{B \times C}\)は、\(B \times C\)という入力から、\(A\)を出力とする射の集まりなので、型定理では\((b,c) \rightarrow a\)となる。

従って、\(A^{B^C}=A^{B \times C}\)は型定理では
\begin{eqnarray}
c \rightarrow (b \rightarrow a) \sim (b,c) \rightarrow a
\end{eqnarray}
となる。これは変数を増やすアンカリー化と変数を減らすカリー化である。

3) \((A \times B)^C=A^C \times B^C\)

左辺\((A \times B)^C\)は、\(C\)という入力から、デカルト積\(A \times B\)を出力とする射の集まりなので、型定理では\(c \rightarrow (a,b)\)となる。

右辺\(A^C \times B^C\)は、\(C\)という入力から\(A\)を出力とする射と\(C\)という入力から\(B\)を出力とする射の集まりのデカルト積なので、型定理では\((c \rightarrow a, c \rightarrow b)\)となる。

従って、\((A \times B)^C=A^C \times B^C\)は型定理では
\begin{eqnarray}
c \rightarrow (a,b) \sim (c \rightarrow a, c \rightarrow b)
\end{eqnarray}
となる。

前回説明したものについても、もう一度、挙げておこう。

4) \(A^0=1\)

左辺\(A^0\)は、\(0\)という入力から\(1\)を出力とする射の集まりである。型定理では、\(0\)は\(Void\)なので、左辺は\(Void \rightarrow a\)となる。

右辺は\(1\)である。型定理では、\(1\)はユニット\(()\)なので、右辺は\(()\)となる。

従って、\(A^0=1\)は型定理では
\begin{eqnarray}
Void \rightarrow a \sim ()
\end{eqnarray}
となる。これは、それぞれの集まりが1であることから、この関係が成り立つことが分かる。

5) \(A^1=A\)

左辺\(A^1\)は、\(1\)という入力から積\(A\)を出力とする射の集まりなので、型定理では\(() \rightarrow a\)となる。

右辺は\(A\)である。型定理では\(a\)となる。

従って、\(A^1=A\)は型定理では
\begin{eqnarray}
() \rightarrow a \sim a
\end{eqnarray}
となる。これは、それぞれの集まりが\(A\)の要素数であることから、この関係が成り立つことが分かる。

6) \(1^A=1\)

左辺\(1^A\)は、\(A\)という入力から積\(1\)を出力とする射の集まりなので、型定理では\(a \rightarrow ()\)となる。これは、終対象への写像であり、写像の総数は1である。

右辺は\(1\)である。型定理では\(()\)となる。

従って、\(1^A=1\)は型定理では
\begin{eqnarray}
a \rightarrow () \sim ()
\end{eqnarray}
となる。これは、それぞれの集まりが\(1\)であることから、この関係が成り立つことが分かる。

最後に型定理とプログラミングの関係を説明した本を紹介しておこう。Benjamin C. PierceのTypes and Programming Languagesがよいと思う(日本語訳も出ているようだ)。彼は、コンピュータ科学の人たちに向けて圏論の本も書いている。
f:id:bitterharvest:20170510203727j:plain

また、最近のホットな話題はホモトピータイプ定理(Hotomopy Type Theory)である。型の概念をさらに抽象化した数学の一分野で、いずれは、コンピュータ科学に大きな影響を及ぼすだろうと期待している。
f:id:bitterharvest:20170511072554p:plain

写像対象-指数対象

7.6 指数対象

写像対象には別の表現法がある。また、こちらの方がよく知られてもいる。それは指数対象と呼ばれる。

対象\(A\)から対象\(B\)への射の集まり\(A \Rightarrow B\)を写像対象と呼んだ。同じように射の集まりなのだが、ドメイン\(A\)を肩に、コドメイン\(B\)をその下に、即ち、\(B^A\)と記述したものを、指数対象という。写像対象と指数対象は記述の仕方が異なるだけで、意味するところは同じである。しかし、指数対象の形で記述すると、何となく馴染みやすい。これは、指数という概念を中学生の時に学ぶので、熟知しているためだ。都合のよいことに、指数対象は指数と概念を共有している。その例を示そう。

ドメイン\(A\)を変えたときに、その指数対象には射がいくつ存在するかを考えてみよう。\(B^A\)は\(A\)から\(B\)への射の集まり(集合)を表している。\(A\)を定めたとき、あるいは\(B\)を定めたとき、その射の集合がどれだけの要素からなりなっているかを考えることにしよう。その時、\(A\)と\(B\)はそれぞれその要素数を表していると考えて解釈する。

まず、ドメイン\(A\)が始対象の時を考えてみよう。Haskellでは始対象は\(Void\)と記述される。これは、ただ一つの関数\(absurd\)という関数を有していた。\(absurd :: Void -> b\)である。Haskellで確認してみる。

Prelude> import Data.Void
Prelude Data.Void> :t absurd
absurd :: Void -> a

始対象は要素を持たないので、その要素数を0である。従って、指数関数が有する射の数は\(B^0\)となる。また、射の数は1個であったので、\(B^0=1\)となる。これは、指数の定義と同じである。

ドメイン\(A\)が要素を一つだけ持つ場合を考えてみよう。これは、Haskellではユニット(Unit)と呼ばれ、\(()\)と記述される。\(()\)からコドメイン\(B\)への射は下図のようになる。
f:id:bitterharvest:20170505083030p:plain
これらの射は定数関数と呼べれるが、その数は\(B\)の要素の数となる。\(A\)の要素は一つなので1とする。そこで、指数関数が有する射の数は\(B^1\)となる。また、射の数は\(B\)個であったので、\(B^1=B\)となる。これも、指数の概念と同じである。

ドメイン\(A\)が要素を二つだけ持つ場合を考えてみよう。これは、ブール値\(\{True, False \}\)となる。このため、指数関数が有する射の数は\(B^2\)となる。射の数は\(B \times B\)個なので、\(B^2=B \times B\)となる。これも、指数の概念と同じである。
一般に、ドメイン\(A\)が要素を\(n\)個持つときは、\(B^n=\prod_{i=1}^{n}B=B \times B \times...B\)となる。

それでは、コドメインの方を変えてみよう。コドメイン空集合の時は、射を定義することができないので、\(0^A=0\)となる。やはり、指数の概念と同じである。

ドメインが一つの要素の時、即ち、終対象、Haskellではユニットの時は、下図のように、関数は一つである。
f:id:bitterharvest:20170505084656p:plain
これから、\(1^A=1\)となる。やはり、指数の概念と同じである。

この章では、数学的な厳密さを追わずに、要素数が同じということで説明したが、次の章ではもう少し数学的な概念を用いて同値であるということを明確にする。

写像対象-Haskellで表現する

7.3 写像対象とは

ここでは写像対象を定義することにしよう。前回の記事写像対象を説明するための図として下図を提示した。
f:id:bitterharvest:20170428074146p:plain
上図で、\(Z\)は最善の表現であるとすると、これは\(A\)から\(B\)への可能な写像を重なることなくすべてを含むような関数の集合であった。これは、\(A\)と\(B\)が定まれば一意に決まるので、\(A \Rightarrow B\)と表すことにしよう。\(A \Rightarrow B\)を縦方向に、\(A\)を横方向にして、その中央には、\((A \Rightarrow B) \times A\)の値を計算する関数を定義する(先の記事ではこれを表で表したが、より、一般的にするため関数とした)。この関数は一意的に定まるので\(eval\)で表す。即ち、上記の図で、\(Z\)は\(A \Rightarrow B\)で表し、\(g\)を\(eval\)で表す。そして、\(Z\)と\(g\)が空席になったので、\(Z’\)は\(Z\)で\(g’\)は\(g\)で書き換えると、下記の可換図式を得る。
f:id:bitterharvest:20170503144407p:plain
この図で、\(A \Rightarrow B\)は関数の集合である。このため、これは対象とみなすことができる。そこで、これを関数対象と呼ぶことにする。なお、上の図が可換図式であることから、\(g\)には次のことが成り立つことが分かる。
\begin{eqnarray}
g = eval \circ (h \times id)
\end{eqnarray}
である。

そこで、上記の可換図式を圏として表しておこう。
①対象:\(A\), \(B\), \(Z\), \(A \Rightarrow B\), \(Z \times A\), \((A \Rightarrow B) \times A\)
②射:\(h\), \(h \times id\), \(g\), \(eval\)
ドメイン、コドメイン:\(h : Z\rightarrow A \Rightarrow B\), \(h \times id : Z \times A \rightarrow (A \Rightarrow B) \times A \), \(g : Z \times A \rightarrow B\), \(eval : (A \Rightarrow B) \times A \rightarrow B\)
④恒等射:\(id_A\), \(id_B\), \(id_Z\), \(id_{A \Rightarrow B}\), \(id_{Z \times A}\), \(id_{(A \Rightarrow B) \times A}\)
⑤合成:\(g=eval \circ (h \times id)\)
また、結合律、単位律が成り立っていることは明らかである。

これで、\(A\)から\(B\)への関数の集合を写像対象として圏として表すことができた。

7.4 Haskellで表すための準備

ここで、対象\(Z\)から関数対象\(A \Rightarrow B\)への射(\(h\)をHaskellの型シグネチャを用いて表すことを考えよう。Haskellでは対象は型(Type)タイプで、射は関数で表す。型シグネチャは関数に入力される型と出力される型を示す。
型が分かっているときは大文字で表される型コンストラクタを用いる(例えば、整数という型であればInt)。また、型がその関数が利用される環境によって決まるときは小文字の型変数を用いる。例えば、2入力、1出力の関数\(f\)の型シグネチャは\(f :: (a, b) \rightarrow c\)で表される。ここで、\(a,b\)が入力、\(c\)が出力である。しかし、入力あるいは出力の中で、型が同じものについては、同じ型変数を用いる。例えば、上記で、2入力、1出力とも同じ型の場合には\(f :: (a, a) \rightarrow a\)とかく。

Haskellでは、関数は関数を入力とすることもできる。今、\(f\)が、1入力1出力の関数を入力するとき、\((a \rightarrow b) \rightarrow a \rightarrow c\)となる。この時、\((a \rightarrow b) \)は入力される関数となり、その次の\(a\)はこの関数への入力である。そして、最後の\(c\)は\(f\)の出力である。なお、型が同じ場合には型変数も同じにするのは前と同じである。

簡単な例を示そう。次のプログラムでは、関数\(dbl\)は関数\(f\)によって得られた値を倍にする。

dbl :: (Num b) => (a -> b) -> a -> b
dbl f a = f a * 2

実行してみよう。

Prelude> :load "dbl.hs"
[1 of 1] Compiling Main             ( dbl.hs, interpreted )
Ok, modules loaded: Main.
*Main> dbl length "abc"
6
*Main> dbl sin 5
-1.917848549326277
*Main> dbl sqrt 4
4.0

ある実数の2乗を出力する関数\(f\)を定義してみよう。

f :: Floating a => (a -> a)
f = \x -> x ** 2

これを実行してみよう。

Prelude> :load "outputFunction.hs"
[1 of 1] Compiling Main             ( outputFunction.hs, interpreted )
Ok, modules loaded: Main.
*Main> f 2
4.0
*Main> f 5
25.0
*Main> f 3.4
11.559999999999999
*Main> f (-2.6)
6.760000000000001

二つの数を入力し、その積をを出力する関数\(g\)を定義してみよう。

g :: Num a => ((a, a) -> a)
g = \ (x, y) -> x * y

これを実行してみよう。

*Main> g (3,4)
12
*Main> g (3.5, 7.8)
27.3
*Main> g (-3.6, -2.5)
9.0

このように、関数の入出力で関数を用いているとき、入出力で用いられている関数は写像対象である。

7.5 写像対象をHaskellで表す

関数の入出力に関数を用いることを学んだので、写像対象の可換図式に現れた射\(h\),\(g\)をHaskellの型シグネチャで表すと次のようになる。

h :: z -> (a -> b)
g :: (z,a) -> b

それでは、関数対象\(A \Rightarrow B\)を定義してみよう。ここでは、前回の記事で説明した例を用いる。例では、\(A\)は\(\{1,2,3\}\)は\(B\)は\(\{T,F\}\)であった。そこで、写像対象\(A \Rightarrow B\)は\(A\)から\(B\)への関数をすべて定義すればよいので、Haskellで表すと次のようになる。

f0 = \a -> case a of 
             1 -> True  
             2 -> True 
             3 -> True
             _ -> error "Not Assigned."
f1 = \a -> case a of 
             1 -> True  
             2 -> True 
             3 -> False
             _ -> error "Not Assigned."
f2 = \a -> case a of 
             1 -> True  
             2 -> False 
             3 -> True
             _ -> error "Not Assigned."
f3 = \a -> case a of 
             1 -> True  
             2 -> False 
             3 -> False
             _ -> error "Not Assigned."
f4 = \a -> case a of 
             1 -> False  
             2 -> True 
             3 -> True
             _ -> error "Not Assigned."
f5 = \a -> case a of 
             1 -> False  
             2 -> True 
             3 -> False
             _ -> error "Not Assigned."
f6 = \a -> case a of 
             1 -> False  
             2 -> False 
             3 -> True
             _ -> error "Not Assigned."
f7 = \a -> case a of 
             1 -> False  
             2 -> False 
             3 -> False
             _ -> error "Not Assigned."

次に、\(Z\)を定義しよう。これは、前回の例では以下の関数を表すものであった(但し、\(Z'\)は\(Z\)に変えてある)。
f:id:bitterharvest:20170504211155p:plain
そこで、対象\(Z\)は関数の名前の集合としよう。即ち、\(Z=\{“f’0”, “f’1”, “f’2”, “f’3”, “f’4”, “f’5”, “f’6”\}\)
次に、\(H:Z \rightarrow (A \Rightarrow B) \)を定義しよう。次のようになる。

h = \z -> case z of
             "f'0" -> f0
             "f'1" -> f1
             "f'2" -> f2
             "f'3" -> f3
             "f'4" -> f4
             "f'5" -> f4
             "f'6" -> f6
             _     -> error "Not Assigned."

さらに、\(g : Z \times A -> B\)を定義しよう。\(g = eval \circ (h \times id)\)より、次のようになる。

g (z, a) = eval (h z, a)
eval (f, a) = f a

可換図式をHaskellで表すと次のようになる。
f:id:bitterharvest:20170503145058p:plain
それでは実行してみよう。

Prelude> :load "fObject.hs"
[1 of 1] Compiling Main             ( fObject.hs, interpreted )
Ok, modules loaded: Main.
*Main> g ("f'0", 1)
True
*Main> g ("f'0", 2)
True
*Main> g ("f'0", 3)
True
*Main> g ("f'1", 1)
True
*Main> g ("f'1", 2)
True
*Main> g ("f'1", 3)
False
*Main> g ("f'1", 4)
*** Exception: Not Assigned.
CallStack (from HasCallStack):
  error, called at fObject.hs:10:19 in main:Main
*Main> g ("f'2", 3)
True
*Main> g ("f'3", 1)
True
*Main> g ("f'4", 1)
False
*Main> g ("f'7", 2)
*** Exception: Not Assigned.
CallStack (from HasCallStack):
  error, called at fObject.hs:50:19 in main:Main

思い通りに機能していることが分かった。

7.5 カリー化とアンカリー化

入出力に関数を用いることを学んだが、関数は一般に\(n\)変数である。そこで、\(n\)変数の関数をそれより一つ少ない変数の関数に次のように変えることをカリー化という。即ち、最初の変数を変数とする関数の戻り値を関数として、これが残りの変数を受けて元の関数と同じ値を返すようにすることをカリー化という。いま、\(f : A_0 \times A_1 \times, ..,\times A_n \rightarrow B\) とした時、\(g : A_0 \rightarrow h\), \(h : A_1 \times A_2 \times, ..,\times A_n \rightarrow B\)となるとき、\(h\)は\(f\)をカリー化した関数と呼ばれる。 また、その逆はアンカリー化という。
カリー化とアンカリー化の例として、ここでは、2変数の関数を1変数の関数に、1変数の関数を2変数の関数に、変えることを考えよう。これを、再帰的に利用すれば、カリー化とアンカリー化を一般化できる。定義に従えば、カリー化\(curry'\)とアンカリー化\(uncurry'\)の関数は次のように定義できる。

curry' :: ((a, b) -> c) -> (a -> (b -> c))
curry' f = \ a -> (\ b -> f(a,b)) 

uncurry' :: (a -> (b -> c)) -> ((a, b) -> c)
uncurry' f = \ (a,b) -> (f a) b

\(curry'\)の定義は次のようになっている。入力が2変数\((a,b)\)出力が\(c\)である関数は、入力\(a\)を受けて、入力が\(b\)で出力が\(c\)の関数を出力する。

それでは、利用してみよう。長方形の面積を求める2入力の\(area\)という関数を定義する。そして、カリー化したときの型シグネチャを求めてみよう。

Prelude> :load "curry.hs"
[1 of 1] Compiling Main             ( curry.hs, interpreted )
Ok, modules loaded: Main.
*Main> area (a,b) = a * b
*Main> :t curry area
curry area :: Num c => c -> c -> c

カリー化した時の型シグネチャは \(Num c => c -> c -> c\)となっている。これは、実は\(Num c => c -> (c -> c)\)と同じである。後者の\(Num c => c -> (c -> c)\)では、最初のタイプ\(c\)の入力を与えると、関数\((c -> c)\)を得る。この関数はタイプ\(c\)の入力を与えると出力\(c\)を得ることを意味する。前者の\(Num c => c -> c -> c\)では、タイプ\(c\)の入力を与えた後で、タイプ\(c\)の入力を与えるとタイプ\(c\)の出力を得ることを意味する。従って、全者と後者は同じである。従って、期待通りにカリー化されていることが分かる。そこで、計算を実行してみよう。

*Main> area (3,4)
12
*Main> curry area 3 4
12

カリー化は、ざっくばらんにいうと、多変数の入力をバラバラにして入力することとなる。

それでは、アンカリー化についても調べてみよう。同じように、面積を求める関数area'を次のように定義する。

*Main> area' a b = a * b
*Main> :t uncurry area'
uncurry area' :: Num c => (c, c) -> c

\(area'\)の定義は、\(area' a b\) は\(area' a\)を実行して関数を得て、この関数に\(b\)を与えて面積を求めることと同じである。即ち、次のように定義しても同じである。

*Main> (area' a) b = a * b

\(area'\)をアンカリー化すると、\((c,c) -> c\)の2入力関数が得られることが分かる。

そこで、これを実行する。

*Main> area' 3 4
12
*Main> uncurry area' (3,4)
12

期待通りになっていることが分かる。

伊豆箱根鉄道駿豆線沿いの遺跡を訪ねる

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

三島市の中心にあるのが伊豆国分寺である。三島駅の隣の三島広小路駅から3分の近さだ。門は新しく、寺の表札も鮮やかだ。
f:id:bitterharvest:20170503211142j:plain
本堂も最近建て替えられたのか綺麗だ。
f:id:bitterharvest:20170503211238j:plain
時代はさかのぼるが、741年に聖武天皇が全国に国分僧寺国分尼寺を建立するように命を出した。伊豆国でも二つの寺が建てられた。僧寺は現在の国分寺の地に建てられたが、現在では、塔跡しか残っていない。本堂の裏に塔の跡がある。
f:id:bitterharvest:20170503211725j:plain
f:id:bitterharvest:20170503211804j:plain

伊豆仁田駅から東へ2km、歩いて25分のところに粕谷(かしや)横穴群がある。静岡県内では最大規模の横穴墓群で、300基あったのではと予想されている。横穴群は函南町の粕谷公園の中にある。子供たちの絶好の遊び場になっていたが、時折、横穴群を目当てに訪れる旅行者も見受けられた。
f:id:bitterharvest:20170503213036j:plain
6世紀から8世紀の200年間にわたって使われたそうだ。後半期には新たに墓は造られず、前からあった墓に追葬が行われたそうである。最後の頃には火葬骨を納めた例もあったとのことである。

墓の内部(玄室)は次のようになっていた。
f:id:bitterharvest:20170503213731j:plain
墓の手前(墓前域)と玄室の間は閉塞石で閉じられていたそうである。墓前域では亡くなった人の霊を慰めるために供養祭が行われたと予想されている。それを示すように、墓前域からはたくさんの土器が出土している。

また、住居跡は見つかっていないそうだが、モデル展示として弥生時代の住居跡や倉庫が展示されていた。
f:id:bitterharvest:20170503214521j:plain
f:id:bitterharvest:20170503214549j:plain

さらには埴輪もモデル展示されていた。
f:id:bitterharvest:20170503214640j:plain

最後は、駿豆線の終点の修善寺駅から旧中伊豆町の方へ4.2Km、歩くと1時間程度かかると思われるところに上白岩遺跡がある。ここは、4000年前の縄文時代中期から後期にかけての遺跡である。ここからは、縄文時代後期を中心とする大規模な配石遺構が発見された。その中に、環状配列の遺構がある。20単位ほどの環状・組石状の小配列が鎖のように連続して並べてあって、直径15mの環状になっている。
次の写真は環状配列である。
f:id:bitterharvest:20170503223839j:plain
別の角度から見ると次のようになる。
f:id:bitterharvest:20170503224023j:plain
組石の写真である。
f:id:bitterharvest:20170503224056j:plain
後ろの方には土壙の跡もある。
f:id:bitterharvest:20170503224312j:plain
環状列石の周りには土壙があり、さらにその外側に住居跡がある。
f:id:bitterharvest:20170503224203j:plain
近くには、長野県の井戸尻遺跡を参考に縄文時代の竪穴住居が復元されていた。
f:id:bitterharvest:20170503224544j:plain
f:id:bitterharvest:20170503224606j:plain
建物の内部には炉があった。
f:id:bitterharvest:20170503224647j:plain
遺跡の全体は次のようになっている。手前二つが住居跡。最後部が環状列石、その手前が組石である。
f:id:bitterharvest:20170503224813j:plain
近くに資料館があったので立ちよる。
入り口近くに、縄文時代の竪穴住居の模型があった。
f:id:bitterharvest:20170503225133j:plain
その横には環状列石の模型もあった。
f:id:bitterharvest:20170503231433j:plain
さらに進むと遺構で発見された縄文時代の土器が展示されていた。
f:id:bitterharvest:20170503225259j:plain
f:id:bitterharvest:20170503225317j:plain
顔面把手も展示されていた。
f:id:bitterharvest:20170503225426j:plain
耳飾りなどの装飾品も飾られていた。
f:id:bitterharvest:20170503225536j:plain
世界最古に属する土器片もあった。
f:id:bitterharvest:20170503225628j:plain
何か怪しい石棒も片隅に置かれていた。
f:id:bitterharvest:20170503225729j:plain

ゴールデンウィークの前半にこれらの遺跡を訪ねた。天気にも恵まれ、富士山の眺望や、柔らかい緑に覆われた里山などが目を楽しませてくれた。

今回は訪問しなかったが、駿豆線に沿って、源頼朝の配流地や、北条氏ゆかりの地、江戸後期の代官であった江川家跡、世界遺産に指定された韮山反射炉などがある。いくつかは既に見学したが、北条氏ゆかりの場所は訪問していないので、次の機会にはぜひ訪れたいと思っている。