bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

むむ?

C内に確実に存在する射とか自然変換達をうまく組み合わせて、[A□X, B] → [A, [X, B] ] という同型射(可逆射)を具体的に構成できればいいのですが、これはなかなか難しいようです。Cがデカルト閉なら、型付きラムダ計算の結果を翻訳して具体的構成ができるかもしれません(僕はやったことありません)。

単純に、これじゃダメでしょうか?(Haskellで書いてますが、文意は推測できると思います。)

f :: ((a,x) -> b) -> (a -> (x -> b))
f h = \a -> \x -> h (a, x)

g :: (a -> (x -> b)) -> ((a,x) -> b)
g h' = \ (a, x) -> h' a x
注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。