「代数系」を含む日記 RSS

はてなキーワード: 代数系とは

2021-01-24

数学科代数系出身だけど、Haskell圏論との繋がりが未だにわからない

Haskell圏論を結びつける主張には前々からずっと疑問を感じている。

およそ、その主張の根拠は「圏論概念であるモナドを借りてきたからだ」というのだが、その言葉意味を突っ込んで追求した人はいないのだろうか。

数学科として、ある程度圏論を学んだ身として疑問に思ってしまうのが、

まり総合的に、「Haskell圏論を用いることで副作用や参照透過性などのプログラミング言語課題解決したのだ」というよくある主張が、全然ピンと来ない。

この辺突っ込んでちゃん解説している専門書はないのだろうか?

第一、第二、第三の疑問いずれに対しても、満足のいく回答は得られず、ただ「モナド圏論由来の概念だ」というだけだ。

もしかして何か、圏論という一般にはよく理解されていない概念言葉を良いように使って、なんだか深淵で素晴らしいもの聞こえるよう、同業者適当にだまくらかしているんじゃないのか?とすら思えてしまう。

2020-01-12

永遠に書きあがりそうもないやつ

何かの参考とかにしたらダメです。書き始めて半年つんだけどこっからどう直したらいいんだか(何をゴールにしたらいいのか)わからない。。

追記:合流性とか強正規化可能性とか停止性とか、全部チューリング不完全で、事前の静的解析で使うメモリの最大量が確定できる、とかそういう風に読み替えられる人を増やしたいのです、数式の添え字とΣと∫にびびらない人を増やしたいようなもの

理論理学の一分野である証明から成長した、数理論理学理論計算機科学境界領域研究領域である型理論(type theory)は、大規模なプログラムの内的な整合性のチェックを行うための方法論を必要とする情報処理技術の分野で関心を集めている。

 そもそも「型」(type)とは何か。プログラミング言語一般的にはレコード関数といったプログラム構成する「値」(value)の定義をする道具である(*1)。その言語コンパイラ作成者はこれらレコード関数などの値、もしくは第一級の対象(first-class object)の種類を区別する型システム(type system)を必要とする。抽象代数学観点からすると、「型」とはこれらの値もしくは第一級の対象が属する高階の対象(higher order object)としての空間(space)ないし代数系(algebraic system)で、型システムはそれら「型」とそれら相互関係(relation)つまり型のなす順序構造(order structure)ないし束構造(lattice structrure)であるといえる。

 プログラム構成する値すべてに型が付くためには、曖昧でない(*2)こと、自己矛盾していないこと、悪循環を含まないこと、それぞれの値の内容をチェックするために無限時間を要しない(*3)ことなどが必要で、これらを満たすなら、プログラムは有限時間で実行を終え、停止する。手続き型言語では無限ループ、型無しラムダ計算では無限再帰によって型付け不能プログラムを書くことができるが、型理論はこれらのチューリング完全な計算機意図しない停止しないプログラムから守る装甲でもあり、再帰メモリ確保で好き勝手をさせないための拘束具でもある。型が付くプログラムには単に停止するというだけでなく、可能な実行経路(訂正:経路→方法)のすべてで同じ結果を出すなど種々の良い性質がある。

1)この定義現実に使われているプログラミング言語の特徴を覆い切れていない、狭い不満足な定義だが本稿では都合上この定義立脚して限定的議論する。例えば変数(variable)というものを持つプログラミング言語もあり広く使われているが、これについてはレコード関数と同じように性質の良いものとして扱うことが難しい。難しさの原因は次の注の内容と関連する。近年は変数を扱うかわりに値の不変のコピー(immutable copy)やその参照に名前を付ける機能を持つプログラミング言語が増えている。

2) 現実情報システムでは、COBOL言語レコード定義C言語の共用体、一般的関数ポインタVisual Basic言語のvariant型変数のように、同一領域に異なる型の値が共存する共用型(union type)の値がしばしば必要となる。共用型の値はgoto文を排除した構造化/オブジェクト指向プログラミングにおいて条件キャストクラス分岐などによる実行経路の複雑さの主要な原因になるが、これは和型(sum type)すなわち相異なる型の非交和(disjoint sum)として定義することで曖昧さな定義できる。

3) ゲームプログラムネットワークサービスにおいてしばしばみられるように、入力として無限リスト任意に深い木のようなものを想定する場合には明らかに(条件を満たさない限り)停止しないことが正しい動作となり、この場合は最外周のループを(←どうする?)メモリリークを起こさないなど別の考慮必要となる。

2015-06-14

C3代数系(代女系?)において,C1,C2で異常な若しくは好き勝手な,自然な振る舞いをしすぎた女が,C1,C2で組にもなろうと思わなかった男に,C3代数系という特殊で人工的な系の中で結婚しましょう=組になりましょうなんてもちかけてきても,すべての男が発情するわけではない。C3代数系は,欠陥だらけである。そもそもC3代数系存在自体が美しくなくて怒る男もいる。

2015-01-11

http://anond.hatelabo.jp/20150111013317

それも別にそういう代数系を考えるだけなわけで、数学範囲なわけだが。

受験用語なんだとすると、いい歳こいた(こいてるよな?文脈からいって)おっさんが「勉強する!」と言って真っ先に発想するのが受験勉強ってことか…。本当に酷いな日本は。

2010-07-19

そのまんま今考えたこととか

RococoWorksの新作の情報が出て、Sun Cagedの新作The Lotus Effectも近いうちに発売らしい。

個人的には実にめでたいことである。

今のうちにカタハネやっとかないとなー。

RococoWorksairy[F]airyの絵がちょっとぺドすぎるんで、カタハネからVolume 7の頃の感じになるといいんだけど。

ワカバみたいな頭巾したロリっ娘が出ないかなぁ。

The Lotus EffectはSun Caged(アルバム)とArtemisia掛ける2を足して2で割ったくらいだったらいいなぁ。

Sun Cagedの方がプログメタルしてるとは思うけど、Artemisiaの湿っぽい情感が好きなんだ。

RenaissanceのBBC Sessionsが欲しいけど、日本コメリカのどっちの密林でも値段が高い。

アニーの声はいいよ。

萌えないけど萌え以上のものがある。

連休を使って実家からアパートに追加の本を送ることにした。

仕事柄ITの本が多いけど、敢えて松坂和夫先生の集合・位相入門と代数系入門も入れた。

それとミルトンエリクソンの本もちょっと。

ジェラルドワインバーグの本は邦訳を7冊持ってるけど、これはいつか原書を読むつもりだから入れなかった。

荷物にはレッド・ツェッペリン再結成クリームDVDも放り込んだ。

キモオタだから昔の音楽がちょっとわかるだけなんだ。

だからツェップとクリーム

ビル・エヴァンスCDを荷物に入れなかったのを激しく後悔した。

 
ログイン ユーザー登録
ようこそ ゲスト さん