Haskell等で使われるLens(の一般形)1は実は論理学とも深い関係がある。Lensの構造に関する研究の(おそらく)最も最初のものはゲーデルのディアレクティカ解釈の研究である2。 ゲーデルのディアレクティカ解釈とは直観主義算術から量化子なしの有限型算術 Tへ…

W. Kneale & M. Knealeのアイデア W.Kneale & M. Kneale, The development of Logic, Clarendon Press, 1962という論理学史の本についてほとんど知られていないであろう内容を書き記しておく1。 この本は古代ギリシアからヒルベルト辺りまでを詳細にカバーし…