関数型プログラミング言語Haskell Part34 (688レス)
前次1-
抽出解除 必死チェッカー(本家) (べ) 自ID レス栞 あぼーん

425: デフォルトの名無しさん [sage] 2024/10/02(水) 22:43:26.42 ID:+kVmY7U4(1/3) AAS
>>424
424(3): デフォルトの名無しさん [] 2024/10/02(水) 22:29:49.51 ID:OPLMo7z3(3/8) AAS
>>422
別の人。自分ならプログラムの記述を一回数学の世界に写すし。

>>423
副作用のある数学的関数ってある?
プログラム→数学
に変換するんだぜ。
副作用のない計算に変換する手順が数学の本に書いてあんの?
別人とのことなので便乗

ID:OPLMo7z3ID:AFS53MaU
> 大文字小文字の変換が自然変換になる事を(Haskellの例で)証明して
と問われて

>>413,414
413(1): デフォルトの名無しさん [] 2024/10/02(水) 20:27:37.99 ID:AFS53MaU(4/6) AAS
>>407
圏論の自然変換だと文字コード前提じゃないので、[0..25] = ['a'..'z'] = ['A'..'Z']ってする。
んで、大文字と小文字は同じ文字の圏、[0..25]は自然数の圏とする。

lCharToInt c = (length.takeWhile (c /=)) ['a'..'z'] -- 小文字からIntへの変換(関手)
uCharToInt c = (length.takeWhile (c /=)) ['A'..'Z'] -- 大文字からIntへの変換(関手)

toLChar = (['a'..'z']!!) -- Intから小文字への変換(関手)
toUChar = (['A'..'Z']!!) -- Intから大文字への変換(関手)

mytoLower = toLChar.uCharToInt -- 大文字から小文字への変換(自然変換)
mytoUpper = toUChar.lCharToInt -- 小文字から大文字への変換(自然変換)

でも、普通のプログラミング言語のtoLower, toUpperも、Char型を圏とみれば同じ。
可換にするのは面倒くさい上に効率悪いけど、そういう関手を作ろうと思えば作れる。
414(1): デフォルトの名無しさん [] 2024/10/02(水) 20:45:45.19 ID:AFS53MaU(5/6) AAS
可換図にすると

   Char(小文字)
  ⇗
Int  ⇑toL ⇓toU
  ⇘
   Char(大文字)

ここで、小文字→Int, 大文字→Intが作れればtoLower, toUpperを直接作らなくても、関手の合成で作れる。
を出してきたのは数学的証明だと思ってるの?
426: デフォルトの名無しさん [sage] 2024/10/02(水) 22:46:45.28 ID:+kVmY7U4(2/3) AAS
>>424
或いはもっと直接的に、>>424は「大文字小文字の変換が自然変換」の真偽をどう考えているの?
429: デフォルトの名無しさん [sage] 2024/10/02(水) 22:55:13.15 ID:+kVmY7U4(3/3) AAS
>>427
427(1): デフォルトの名無しさん [] 2024/10/02(水) 22:51:00.95 ID:OPLMo7z3(4/8) AAS
定義が何もないのに何も言えるわけないじゃん。
数学でこういうものを定義します、これをプログラムのこれこれと対応付けます。
てプロセスないじゃん。
了解

>>422
422(2): デフォルトの名無しさん [sage] 2024/10/02(水) 22:20:07.75 ID:sFAdPyYV(1) AAS
ID:OPLMo7z3 = ID:AFS53MaU 本人か同レベル

複おじってレベル
の指摘通りだと納得しました
前次1-
スレ情報 赤レス抽出 画像レス抽出 歴の未読スレ AAサムネイル

ぬこの手 ぬこTOP 1.395s*