Haskell等で使われるLens(の一般形)¹は実は論理学とも深い関係がある。Lensの構造に関する研究の(おそらく)最も最初のものはゲーデルのディアレクティカ解釈の研究である²。

ゲーデルのディアレクティカ解釈とは直観主義算術から量化子なしの有限型算術 Tへの翻訳のことである。ちなみにこの「ディアレクティカ」というのは論文誌の名前であり、その内容で名付けられているわけではない³。

なぜそのような解釈を考えたかというと、古典算術の無矛盾性証明をヒルベルト流の有限の立場(を拡張した立場)から行おうとしたからである。古典算術の無矛盾性は彼の二重否定翻訳によって直観主義算術を経由することでTの無矛盾性に還元することができる。それだけではなくこの翻訳を通じて古典算術や直観主義算術上の証明の構成的な情報を抽出することもできる。

Lensに関してはディアレクティカ解釈 $(-)^{D}$ で最も重要なのはその含意の解釈である。

$(A\Rightarrow B)^{D}=\exists T Z \forall u v [A_{D}(u, Z(u, y))\Rightarrow B_{D}(T(u), y)$ ]

ここで $T:U\to V$ と $Z: U\times Y\to X$ は新しく導入される汎関数。

ディアレクティカ解釈とレンズの対象及び射を明確に結びつけたのはValeria de Paivaのディアレクティカ圏DCの定式化である。

有限極限を持つ圏Cから構成されるディアレクティカ圏DCの対象はモノ射 $A\hookrightarrow^{\alpha} U\times X$ で⁴ ( $A, U, X \in C$ )、射は $A\hookrightarrow^{\alpha} U\times X$ , $B\hookrightarrow^{\beta} V\times Y$ に対して、Cの射の組 $f: U\to V$ と $F: U\times Y\to X$ であり、pullbackに関するある条件を満たすものである(p.3)。

類似性は一見して明らかである。

ここで対象を $A\hookrightarrow^{\alpha} U\times U$ の形のモノ射に限定すると、射は $A\hookrightarrow^{\alpha} U\times U$ , $B\hookrightarrow^{\beta} V\times V$ に対して、射の組 $f: U\to V$ と $F: U\times V\to U$ となる。これでlens圏の定義⁵のget: $U\to V$ とset: $U\times V\to U$ と同じになった。カリー化させるとよく見かけるレンズの形となる。

get :: U -> V 
set :: U -> V -> U

線形論理との関連

Hedgesの論文Limits of bimorphic lensesによればbimorphic lenses⁶はディアレクティカ圏の公理を満たすようである。

"The fact that Bilens is a degenerate dialectica category was pointed out to the author by Dusko Pavlovic (private communication)" (p.3).

Paivaは論文でディアレクティカ圏DCは直観主義線形論理の圏論モデルであることを証明しているので(p.20)、これらを合わせるとレンズ圏(bimorphic lensesの圏)は直観主義線形論理のモデルとなっている。

参考文献

A.Blass, A geme semantics for linear logic, Annals of Pure and Applied Logic, vol.56, issue 1-3, 183-220, 1992.

https://www.sciencedirect.com/science/article/pii/0168007292900739

K.Gödel. "Uber eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes - Dialectica", dialectica, pp280-287, 1958. (Translation and analysis in Collected Works Vol II Publications 1937-1974, eds S. Feferman et al., Oxford University Press, pp.241-251, 1990).

https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1746-8361.1958.tb01464.x

J.Avigad and S. Feferman. Gödel's functional (“Dialectica”) interpretation. Handbook of proof theory, eds. S. R. Buss, Studies in logic and the foundations of mathematics, vol. 137, Elsevier, pp. 337–405, 1998.

J.Hedges, Lens for philosophers, blog post, 2018.

https://julesh.com/2018/08/16/lenses-for-philosophers/

J.Hedges, Limits of bimorphic lenses, arXiv, 2018.

https://arxiv.org/abs/1808.05545

V.de Paiva, The dialectica categories. Technical report, University of Cambridge, 1991.

https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=&cad=rja&uact=8&ved=2ahUKEwiW1vP01r7wAhWKFIgKHXJ6DTkQFjADegQIAxAD&url=https%3A%2F%2Fwww.cl.cam.ac.uk%2Ftechreports%2FUCAM-CL-TR-213.pdf&usg=AOvVaw1F7ySqn-5cWMV3Q43ugbvN

nLab, blogpost

https://ncatlab.org/nlab/show/lens+%28in+computer+science%29

日本語文献

藤原誠, 数学基礎論サマースクール2018スライド, 2018.

http://www2.kobe-u.ac.jp/~mkikuchi/ss2018.html

木原貴行, 2019 年度数理情報学基礎論概論 2・講義ノート.

http://www.math.mi.i.nagoya-u.ac.jp/~kihara/pdf/teach/fom2019spring.pdf

白旗優, ダイアレクティカ解釈, ゲーデルと 20 世紀の論理学 3 (不完全性定理と算術の体系), 第 III 部, pp.205–274, 2007.

http://hackage.haskell.org/package/lens-3.7.1.2
http://hackage.haskell.org/package/lenses-0.1.6 ↩
もちろんlensという用語は用いていない。この記事はHedges, 2018の記事を参照している。
https://julesh.com/2018/08/16/lenses-for-philosophers/↩
もっとも、ゲーデルのディアレクティカ解釈はゲーム意味論とも関連があるので(Paiva, 及び Blassの論文を参照)、結果的にディアレクティケー(対話)と関係があった。↩
より正確に理解したいならば下記の文献を参照。↩
https://ncatlab.org/nlab/show/lens+%28in+computer+science%29 ↩
対象と射はディアレクティカ圏のものを考えれば良い。↩

Asinus's blog

西牟田祐樹のブログです。

Lensを通して見るゲーデル

線形論理との関連

参考文献