やったこと

シャニ

黒セーラの灯織のTrue。
Sランクで親愛Maxなのでいい感じなのでは。
コミュも良かった。

https://twitter.com/make_now_just/status/1355550860583993351

あとフェスイベントを終わらせた。
最近シャニをやる時間がない。

minicheck

色々考えたら思い付いてしまった。
天才かもしれない。

$R$ を乱数生成器として、$g_A : R \to (R \times A)$ を型 $A$ の値を生成する生成器オブジェクトとする。
$a \in A$ について $g_A(r) = (r', a)$ となる $r \in R$ が存在するとき、$g_A$ は $a$ を生成可能といって$a \mathrel{\tilde\in} g_A$ で表す。
このとき任意の $a \in A$ について $a \mathrel{\tilde\in} g_A$ のとき $g_A$ は網羅的である、という。
当然だが、生成器オブジェクトは網羅的であることが望ましい。

$c_A : \forall B.\ (R \to (R \times B)) \to (R \to (R \times (A \mathrel{\tilde\to} B)))$ を $A$ に対するco-生成器オブジェクトとする。
ただし $A \mathrel{\tilde\to} B$ は $A$ から $B$ への部分関数を表すデータ構造の全体からなる集合とする。
$c_A$ と $g_B$ があるとき、$A$ から $B$ への関数を生成する生成器オブジェクト $g_{\to}(c_A, g_B)$ を構成できる。

$g_A$ について $g_{\ast}(g_A) : R \to (R \times A^\ast)$ を $A$ の値の列 (リスト) を生成する生成器オブジェクト、
$c_A$ について $c_{\ast}(c_A) : \forall B.\ (R \to (R \times B)) \to (R \to (R \times (A^\ast \mathrel{\tilde\to} B)))$ を $A$ の値の列に対するco-生成器オブジェクトとする。

$g_A$ と $c_B$ が与えられたときに、
$c_{\to}(g_A, c_B) : \forall C.\ (R \to (R \times C)) \to (R \to (R \times ((A \to B) \mathrel{\tilde\to} C)))$ を構成できるだろうか？
考えられる1つの方法として、次のHaskell風の疑似コードで説明されるようなものがある。

つまり、$A$ の値と $B \to C$ の関数を生成しておいて、渡ってきた $A \to B$ の関数に $A$ の値を、その返り値を $B \to C$ の関数に渡すことで、最終的に $C$ の返している。

これは一見上手く動作しそうだが、実際には網羅的ではないという問題がある。
具体的には、この方法では $A \times C^B$ 種類の値しか生成できないが、 $(A \to B) \to C$ の値の種類は $C^{B^A}$ 程度あるので、必然的に漏れが存在することになるわけである。

ここで1つの事実を確認する。

$B^\ast$ には $A \to B$ と同型となる部分が存在する。

つまり $A = \{ a_1, a_2, \cdots \}$ とおいたとき、 $f : A \to B$ があれば $[f(a_1), f(a_2), \cdots]$ として $B^\ast$ の元が得られて、反対に $[b_1, b_2, \cdots]$ があるとき $f(a_k) = b_k$ として $f$ を構成できる。

よって $B^\ast \to C$ は $(A \to B) \to C$ よりも真に大きい。
これを利用して、次のような疑似コードで説明する方法を考える。

つまり、 $A$ の値の列と $B^\ast \to C$ の関数を生成しておいて、渡ってきた $A \to B$ の関数に $A$ の列の各値を適用して、その返り値の列を $B^\ast \to C$ の関数に渡すことで、最終的に $C$ の値を得ている。

この方法ならば、各生成器オブジェクトやco-生成器オブジェクトが網羅的に機能していれば、こちらも網羅的となる。
しかし、列の生成器オブジェクトは重複する値を持つ列を生成する可能性があるが、そのようなものはこの場合では無駄である。
そこで、次の値の重複しない $A$ の列を生成する生成器オブジェクト $g_{\le}(g_A)$ を $g_{\ast}(g_A)$ の代わりに用いれば良いのではないかと思われる。

というのが今のところの考察となる。
かなり良く考えられているのではないかと思う。
単一の値の代わりに列や集合を渡す、というのはわりと思い付くアイディアかもしれないけれど、それをちゃんと意味付けできたことに意義がある。

が、いくつかあやしいところもあって、例えば「$B^\ast$ には $A \to B$ と同型となる部分が存在する」というのは $A$ が有限集合じゃない場合かなり嘘っぽい。
まあ無限リストが許されるなら可算集合でもいけると思うけど、非可算な場合はどうすればいいのか検討もつかない。
とはいえ、コンピュータで表現できるデータが非可算になったりするのかもよく分からないので何とも言えない、という感じ。

どうにか昇華した感じがする。楽しいね。