表示的意味論
概要
プログラムを数学的対象に翻訳する。
もしくは、別の言語に翻訳する。
特に関数型プログラミング言語に対する意味論として あつかわれる ことが おおい。
slogan: a program denotes a math object.
特徴
なお、実行時の動的な意味論が欲しい なら、やはり操作的意味論が必要に なる。 複数のプログラミング言語を同一言語に翻訳することで、比較が しやすくなる。
モチベ
再帰するので難しい
ここでは、表示的意味論 = 領域理論
「使う」という関係だなwint.icon
用語
domain: 領域
syntax: 文法、形式言語
表示函数
概念
data vs process
static vs dynamic
合成性 (Compositionality)
環境
関数
再帰的定義
つまり、グラフではない
部分関数
lifting: with ⊥
領域
つまり整数同士には情報量に差がない（順序が未定義）
未定義⊥が最小元
メタなラムダ抽象
table:domains
data CPO
process continuous functions (on CPO)
近似
$ \sqsubset: 意味近似順序 (semantic approximation order)
$ \bot = f_0 \sqsubseteq f_1 \sqsubseteq f_2 \sqsubseteq \ldots
概念
lazy natural numbers
葉の系列が 自然数N全体への近似に なってる。
https://www.researchgate.net/profile/Albert-Meyer/publication/2306163/figure/fig1/AS:669388697006081@1536606110489/1-The-poset-of-lazy-natural-numbers-where-S-denotes-the-lazy-successor-function.png
具体例
toy model
資料
表示的意味論が哲学において持ちうる重要性について考察したい
連続関数についていえばその不動点を計算する手続きがあれば、その表示的意味が取れる
対照的に、純粋関数型言語の意味はデフォルトで実行の方法から完全に独立しています。 Haskell98の言語仕様でさえ、Haskellの非正格な表示的意味論だけで規定されており、実装方法については規定されていません。
正格言語の領域は全て平坦
横内『プログラム意味論』