この記事は Haskell Advent Calendar 2020 20日目の記事です．
TL; DR
タイトル
続きを読む引数で受け取った値を通じてのみ値を構築することを強制するランク2多相を使ったテクニック
Dhall の Prelude を眺めていて見付けた，ランク2多相を使ったテクニックを紹介する．
続きを読む『形式意味論入門』を Haskell に書き下す (前編)
一昨年のゴールデンウィークに池袋のジュンク堂を訪れた際，『形式意味論入門』という表題の本に目が止まり，数学や論理学を用いて自然言語表現の意味を形式的に考察する学問分野があることを知った*1．また，その道具立てとして単純型付きラムダ計算が用いられていることが，なおのこと私の興味を惹いた．ラムダ計算といえば，読者の多くが計算機科学分野での応用を思い浮かべると思うが，Richard Montague*2 が自然言語分野に応用して以来，そちらの方面でも道具立てとして用いられているようである．
- 作者:拓郎, 田中
- 発売日: 2016/09/20
- メディア: 単行本
この本は，Irene Heim と Angelika Kratzer による Semantics in Generative Grammar (以下 Heim and Kratzer) をベースに書かれているのだが，Heim and Kratzer で用いられる意味計算規則のうち，実質的に用いられるものはたった4つであるとし，前半で4つの意味計算規則の導入を行い，後半ではその他の自然言語現象に対して形式的な意味を与えていく，という構成になっている．また，統語論を学んだ人文科学系の学生を対象読者として書かれているため．序盤では集合論やラムダ計算に関する非形式的な説明に文量が割かれている．
この記事は，私が『形式意味論入門』の内容の習得を試みる際に，自分の理解が正しいかを確かめるため，Haskell のコードとして書き下した内容を下地に書かれている．言語表現及びそれらの外延をプログラム，とりわけ Haskell のプログラムにエンコードするメリットとしては，
- 意味計算を自力で行う必要がない
- 型の整合性が GHC の型検査機によって自動的に保証される
などが挙げられるだろう．
この記事は前後編に分かれている．前編では，事前知識の導入の後，4つの意味計算規則のうち最初の2つを導入する．後編では，更なる準備の後，残る2つの意味計算規則を導入する．
*1:ちなみに，意味論を研究する研究室に所属する友人に聞いたところ，形式意味論の入門に当たっては，Elements of Formal Semantics がおすすめだそうである．
*2:アメリカの数学者，哲学者．博士課程時代には Banach-Tarski のパラドクスで知られる Alfred Tarski の門下で公理的集合論を研究．その後，数理論理学を自然言語の意味論に応用する研究に着手し，今日の形式意味論の草分け的存在となった．