[過去ログ] 関数型プログラミング言語Haskell Part33 (1002レス)
前次1-
抽出解除 レス栞

このスレッドは過去ログ倉庫に格納されています。
次スレ検索 歴削→次スレ 栞削→次スレ 過去ログメニュー
リロード規制です。10分ほどで解除するので、他のブラウザへ避難してください。
754
(1): 2021/02/25(木)20:48 ID:zWeVIvWn(1) AAS
ある対象がモノイドかどうかを問う質問です。

2つのリストのうち要素の少ない方のリストをそのまま返す、
同じ要素数ならば左側のリストをそのまま返す関数 f :: [a] -> [a] -> [a] があるとします。
ここで、ある型aのリスト全体の集合[a]と、その上の二項演算fとの組([a], f)はモノイドを成すでしょうか。

私は次のように、これはモノイドではないと考えます。

このモノイド性を考えるとき、その単位元の候補として、
もし集合に無限リストを含めないのならば最大要素数のリストを、
無限リストを含めるのであれば無限リストを取ります。
他に考えようがありません。

しかし、どちらにしても単位元の一意性が証明できません。
xs、ys 共に最大要素数のリスト、あるいは無限リストであり、かつ xs /= ys を満たすものは(型aによっては)いくらでもあります。

よって、([a], f) はモノイドではないと考えますが、これは正しいでしょうか。

モノイドの定義に照らし合わせるのではなく、
モノイドならば証明できるであろう定理が証明できないことに因っているのが、
なんとも気持ち悪いのですが・・・

そもそもモノイド性を問うには ([a], f) の定義が曖昧なのでしょうか。
759
(1): 2021/02/26(金)10:24 ID:nFSf/y++(1) AAS
>>754
まず単位元の定義から、esが[a]の単位元であるなら、任意のxsに対して
f es xs == xs
f xs es == xs
を満たす、というところはいいよね(ゆえにesは、任意のxsより要素数が大きくなければいけない)

このことから直接非存在を言う方がこの場合は明快だと思うけど、
「ある要素が単位元ならばそれが一意である」はすぐに言えるから
背理法により単位元が存在しない、でも正しい論証だと思う

もしこの演算fに対してモノイドを構成するなら、
(>>756とほぼ同じことを言うが) length es == ∞ なる要素を1つ決めて
(全ての有限リスト) ∪ {es}
みたいな集合の上でなら言えそう
ちゃんと見てないけど結合律もそれっぽく振る舞ってそう
前次1-
スレ情報 赤レス抽出 画像レス抽出 歴の未読スレ AAサムネイル

ぬこの手 ぬこTOP 0.038s