集合論に基づいた言語を作りたい

**デフォルトの名無しさん** · 2014/08/10(日) 21:27:16.56

計算機科学の基礎は集合論であるという。
ならば、集合論に基づいた言語を作れば美しい言語になるのでは？
そんな発想から徹底的に集合論的思想で言語仕様を考えるスレです。

**デフォルトの名無しさん** · 2014/09/30(火) 22:19:13.15

>>398
わざわざスレを立てなくても集合論プログラミングでググればすぐ見つかるんだけど。
「発想から徹底的に集合論的思想で言語仕様を考える」と言っておきながら
その程度の検索すらしてなかったんだな。

１ · 2014/09/30(火) 22:29:12.29

>>399
まあな。

**デフォルトの名無しさん** · 2014/09/30(火) 23:59:40.07

>>397
アルゴリズムの自動生成をするわけではなく、論理式を使って書かれた
仕様を元にして人間がプログラムを作っていくもので、VDMやZと同じ
方向なんだけど、感想がずいぶん違うな。>>384 >>398

１ · 2014/10/01(水) 06:02:07.09

>>401
VDM　書いたものが実装にならない
集合論プログラミング　書いたものが実装になる

と思い込んでたからな。
どっちも書いたものが実装にならないならあんまり俺の趣味じゃないなぁ。
集合論プログラムは書いたものが実装になってもよさそうなほど
論理を詰めていたように見えたが気のせいだったか。

**デフォルトの名無しさん** · 2014/10/01(水) 09:03:58.23

>>402
VDMは実行可能だ

**デフォルトの名無しさん** · 2014/10/01(水) 11:04:19.89

>>398
やっぱりアンタはセンスが良い。というかこれから何かできる人だ。
集合論プログラミングはZなんかに比べるとマイナーだが、Zより実質がある。
実装もできる。アンタが土台にするべき言語はこれじゃないかな？
検索してないとかなんとかというノイズは無視していいよ。

**デフォルトの名無しさん** · 2014/10/01(水) 14:56:19.11

>>402
論理式を使って、プログラムに自動的に変換できそうなほど詳細な仕様を書くのは、
＞緩い感じでコーディングして仕様変更があってもちょちょっとハッキングすれば
＞何となく動いちゃうみたいの
とはかなり違うわな。

1 · 2014/10/01(水) 19:43:26.77

>>403
どうゆう意味で実行可能なの？
他のプログラムの外付けアサート的な動作しかできないのかと思いこんでいたが。
VDM単体で動くの？

>>404
俺をおだてても木には登れんぞ。
集合論プログラムのコンパイラを作るなんて俺の実力じゃとても出来そうもない。
ユーザーとしてなら使ってみたいが。

>>405
仕様を詳細にするのはやり方がまずいと柔軟性のないプログラムになると思う。
抽象度の高いプログラムで仕様を満たせるならそっちの方がいいと思う。

**デフォルトの名無しさん** · 2014/10/01(水) 19:49:09.29

>>406
インタプリタで実行できる

１ · 2014/10/01(水) 20:28:28.86

>>407
まじで。英語だからちゃんと読んでないけど>>360のwikiにsqrtの例で

SQRT(x:nat)r:real
post r*r = x

とかいうのがあったからこりゃ単体じゃ実行できないなと思ったんだけど。
早計だったか。

**デフォルトの名無しさん** · 2014/10/01(水) 20:39:41.94

>>408
VDMには実行できるexplicit specと実行できないimplicit specがある。
その例は実行できないimplicit specのほう。
このリンク先のはみな実行できるexplicit spec
http://www.vdmtools.jp/doc/tips/vdmIdiom.html

１ · 2014/10/01(水) 21:57:06.59

>>409
なんか、サンプルプログラムよんでもイメージが湧きづらい。。。
文字列操作の前後のスペースをトリミングとか何やってるのかよく分からん。

[ p | p in set inds org & org(p) <> ' ']がorgの空白でない文字のインデックスの集合で
パターンマッチでその集合の先頭と末尾を取り出してる。
sがorgの空白じゃない最初の文字のインデックスでeがorgの空白じゃない最後の文字のインデックス
でorg(s,...,e)で頭とおしりの空白を取り除いた文字列を返してるってこと？

１ · 2014/10/01(水) 22:21:29.56

[]は集合じゃなくて列か。

**デフォルトの名無しさん** · 2014/10/01(水) 23:50:12.62

>>409
クソVDMなんか持ってくるんじゃねえよ。
お前はセンス悪い。

1 · 2014/10/02(木) 12:38:59.14

あれ？乗っ取られてる？立てただけでちょっと居なくなったすきに…

１ · 2014/10/02(木) 18:33:20.87

>>413は偽物。
といっても俺も本物だと証明できるものはなにも持ってないな。
まあ、何が本当かは皆さんの判断に任せるとしましょう。

**デフォルトの名無しさん** · 2014/10/02(木) 19:01:12.47

ここって>>1となれ合うスレ化してるから、馴れ合ってる1こそが1

**デフォルトの名無しさん** · 2014/10/02(木) 19:52:03.79

>>414
トリップっていうのをつけたら?
http://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q1241152992

１ · 2014/10/02(木) 20:07:14.68

>>416
今からトリップつけても過去のスレに対してはなんの証明にもならんけどな。
今からでもみんなが付けろっていうなら付けるが。

**デフォルトの名無しさん** · 2014/10/02(木) 20:38:47.31

>今からトリップつけても過去のスレに対してはなんの証明にもならん
それは>>415のように考えるしかない。

１ · 2014/10/02(木) 20:45:42.53

>>418
まじでｗ

１ · 2014/10/03(金) 20:31:44.20

Rubyだとトリミングはstr.stripで一発だな。
ライブラリつかわんでもstr.gsub(/^ +/,"").gsub(/ +$/,"")でワンライナーか。
この比較がフェアかどうかは微妙だが、Rubyと比べてVDMは読むのしんどいな。
慣れてないだけかもしれんが。

**デフォルトの名無しさん** · 2014/10/03(金) 22:20:11.35

>>420
的外れな比較だな。

１ · 2014/10/03(金) 22:25:06.66

>>421
やっぱそうか。そんな気はした。
でもこういったこまごまとした道具がきっちりそろってるのもRubyの魅力なんだよな。

**デフォルトの名無しさん** · 2014/10/04(土) 04:41:52.82

で、文字列をトリミングするのが君のいう集合論ベースの言語なのかい？

１ · 2014/10/04(土) 09:55:23.27

>>423
トリミングについてはちょっとふれただけだろ。
そんなに粘着した覚えはないぞ。

**デフォルトの名無しさん** · 2014/10/04(土) 12:53:49.48

言ってることがブレブレなんだよ。
集合論から徹底的にと言ってみたり有限集合だけと言ってみたり
言語仕様だと言ってみたり便利なライブラリだと言ってみたり
美しい言語だと言ってみたり処理速度がどうのと言ってみたり
で、今度は文字列操作ユーティリティライブラリの充実度か。

結局何がしたいんだ？

**デフォルトの名無しさん** · 2014/10/04(土) 13:00:56.11

有限集合のみだと素朴集合論以下だしな。

**デフォルトの名無しさん** · 2014/10/04(土) 13:34:13.41

>>425
そんなに結論を急ぐのはなんでなの？

**デフォルトの名無しさん** · 2014/10/04(土) 14:11:28.47

結論どうこう以前に
こうまで毎回後だしジャンケンばかりでは
永遠にグダグダだろ

**デフォルトの名無しさん** · 2014/10/04(土) 16:04:23.04

個人のチラ裏にそんな文句つけてやるなよ

**デフォルトの名無しさん** · 2014/10/04(土) 16:08:30.01

ID:TsYLxX57の書き込みに文句をつけるのもなしの方向で

１ · 2014/10/04(土) 16:10:38.32

>>425
何がしたいかといわれると、建前では教科書の章末問題のようなものを
サクサクインプリメントできる言語をつくりたいだが、本音を言えば>>386だな。

まあ、集合論に基づいた言語自体、まだ形がほとんど何もできてない状態だから
議論がぶれるのはある程度しかたないな。

>>428
後出しジャンケンといわれても困るんだが。

**デフォルトの名無しさん** · 2014/10/04(土) 16:17:38.75

何の教科書だよ。
集合論に基づいた言語と言うから集合論の教科書かと思ってたら
集合論の教科書は想定してなかったとか言い出すし。

１ · 2014/10/04(土) 16:23:04.72

>>432
まあ、主に離散数学だな。

**デフォルトの名無しさん** · 2014/10/04(土) 18:36:28.77

zfcに基づいたプログラミング言語は理論上作成可能？

**デフォルトの名無しさん** · 2014/10/04(土) 19:35:13.51

論理言語なんてPrologでええやん

**デフォルトの名無しさん** · 2014/10/04(土) 19:46:48.95

基づくというだけなら既存のスクリプト言語のsetクラスでも、基づいているとは言えるんじゃね？
ZFCで表現可能な全ての集合を扱える、という条件なら、無理だろ。

**デフォルトの名無しさん** · 2014/10/05(日) 18:24:35.09

>>434
そりゃ可能だよ。既にだれか作ってたような

**デフォルトの名無しさん** · 2014/10/06(月) 01:43:06.63

選択公理は無理だろ。
無限公理もキツイと思う。

**デフォルトの名無しさん** · 2014/10/06(月) 12:01:11.94

選択公理って、よーするに、どんな集合からでも「その要素を一つ選んで取り出す」ことができる、
とする公理でしょ。コンピュータでそれを原理として使えない理由ってある？

（本物の実数の濃度を持った集合を表現できない、とか？）

**デフォルトの名無しさん** · 2014/10/06(月) 12:36:12.97

「無限集合の無限集合」をどう扱うよ？

**デフォルトの名無しさん** · 2014/10/06(月) 12:55:54.86

（ポインタで表される）一つの要素であることに変わりは無いと思うけど

**デフォルトの名無しさん** · 2014/10/06(月) 13:25:58.86

…解らないなら解らないと正直に言えばいいのに…

**デフォルトの名無しさん** · 2014/10/06(月) 15:33:29.23

説明できないなら（以下略

**デフォルトの名無しさん** · 2014/10/06(月) 15:44:15.26

選択公理は選択する方法があるとは主張するけど、選択する方法を具体的に出す訳じゃないから無問題

**デフォルトの名無しさん** · 2014/10/06(月) 22:35:03.81

>439
可能無限なら扱える。実無限は無理。

>441
自然数で番号付けできているから、実数は扱えない。

>444
実数は選択できないよ。

**デフォルトの名無しさん** · 2014/10/06(月) 22:39:52.81

哲学屋が語る論理の本で勉強したなw

１ · 2014/10/06(月) 23:54:52.31

なんか計算不能な問題に取り組ませたい奴がいるっぽいな。
>>48と同じ奴か？

**デフォルトの名無しさん** · 2014/10/07(火) 00:54:44.71

スレタイに釣られるとそうなるよ

**デフォルトの名無しさん** · 2014/10/07(火) 05:00:08.90

DaOiROEZの半可通っぷりが最高w

**デフォルトの名無しさん** · 2014/10/07(火) 10:56:48.49

ZFの範疇でさえ消化できてないのに、実無限なんて飛躍しすぎ。

**デフォルトの名無しさん** · 2014/10/07(火) 11:06:53.72

どうせなら、量子コンピューターで使う言語にまでにして欲しいな。

１ · 2014/10/07(火) 21:14:56.86

量子コンピュータってまだ有効なアルゴリズムが２つ３つしか発見されてないんじゃなかったけ。

**デフォルトの名無しさん** · 2014/10/07(火) 21:30:05.48

量子状態を集合的に扱うと便利。

**デフォルトの名無しさん** · 2014/10/07(火) 21:41:15.48

>450
少ない公理だけでやるんだったらProlog (HornCNF) で十分だと思う。
というかPrologがろくに検討されていないのはなぜ？

１ · 2014/10/07(火) 22:20:49.79

Prologもやってみる価値あり？

**デフォルトの名無しさん** · 2014/10/08(水) 04:21:45.13

公理論ベースのプログラミング言語というのにPrologを検討してないとか意味わからなすぎ

**デフォルトの名無しさん** · 2014/10/08(水) 11:09:43.78

単なる述語論理じゃないか。

**デフォルトの名無しさん** · 2014/10/08(水) 12:20:34.72

>>1ってそもそも集合論、公理的集合論を系統的に学んだこと無いだろ？

**デフォルトの名無しさん** · 2014/10/08(水) 12:47:37.54

既存の言語に有限集合演算を追加するところから始めれ。
クソスレが一個増えただけで終わる前に。

**デフォルトの名無しさん** · 2014/10/08(水) 18:43:36.24

ここは元々>>1の勉強ｽﾚ

1 · 2014/10/08(水) 18:47:59.90

>>458
ばれたか。ZFCとか名前くらいは聞いたことあるけど
どうやって論理を展開していくのとか知らない。

>>459
出来ればもうちょっと面白いアイディアが欲しい。
クソスレも板の賑わいってことで。

**デフォルトの名無しさん** · 2014/10/08(水) 20:19:42.08

1が今まで読んできた教科書教えて

１ · 2014/10/08(水) 20:46:16.58

あんまりいうと個人情報とか洩れるかもしれんので一つだけ。
もう捨てちまって手元にないがこれかな。
http://www.amazon.co.jp/dp/4274130053

**デフォルトの名無しさん** · 2014/10/08(水) 22:26:27.29

じゃあ個人情報が漏れない程度の大雑把さで何を学んできたか教えて

１ · 2014/10/08(水) 22:32:55.73

そんな漠然としたこと聞かれても。
まあ、情報系の学部出身だよ。

**デフォルトの名無しさん** · 2014/10/08(水) 23:00:13.01

人生……かな

**デフォルトの名無しさん** · 2014/10/08(水) 23:04:08.42

>>59を見てどの程度の知識があるのか気になったのよ
数学科ではないのね

１ · 2014/10/08(水) 23:24:26.28

数学科ではないな。
まあ、俺は数学ガチ勢ではないってことで。

**デフォルトの名無しさん** · 2014/10/08(水) 23:51:56.29

>>465
それにしてはレベルが低いな。

**デフォルトの名無しさん** · 2014/10/09(木) 14:59:21.86

>スクリプト言語でありながら、速度も求めた Julia という言語。
> Julia は科学技術計算向けだが、汎用的な用途にも使える。
http://julialang.org/

集合論とはちょっと違うが、こういう言語を作るのって、プログラミングとはまた別の頭の良さが必要なんだろうなあ・・・

**デフォルトの名無しさん** · 2014/10/09(木) 18:53:47.65

>>463
こんなの学部一、二年だろ？
http://www.amazon.co.jp/Constraint-Logic-Programming-Selected-Research/dp/0262023539
こういうの読みなよ。

**デフォルトの名無しさん** · 2014/10/09(木) 19:18:35.22

constraint logic programming‥

メジャーなもののなかで一番近い言語はなんですか

**デフォルトの名無しさん** · 2014/10/09(木) 19:25:16.95

これのOｚだよ。
http://www.amazon.co.jp/dp/4798113468/

１ · 2014/10/09(木) 20:10:14.35

>>469
こんなもんじゃね？

>>470
インタプリタでCに迫る速度とかホンマかいな？
まあ、速くて書きやすいのはいいことだ。

>>471
わざと難しそうなの持ってきてない？

**デフォルトの名無しさん** · 2014/10/11(土) 12:51:05.92

この板でハッとさせられるような事言う奴滅多にいないんだよな。
たまに居ると思ったら５年前の自分の書き込みだったw

**デフォルトの名無しさん** · 2014/10/11(土) 13:27:28.71

>>475
つまり、おまえは5年間進歩してないんだな。

**デフォルトの名無しさん** · 2014/10/11(土) 15:22:20.55

とっくに出てると思うけど、SQLがまさに集合論をベースとしてる
今ではC#がLINQという名前で取り込んでるな

**デフォルトの名無しさん** · 2014/10/11(土) 16:17:13.48

それは集合論ではない。
集合や集合演算を扱えるだけ。

**デフォルトの名無しさん** · 2014/10/11(土) 17:10:54.15

>>477
それSQLじゃなくてRDBシステムが集合論つかってるってことじゃないのか？

**デフォルトの名無しさん** · 2014/10/11(土) 18:08:16.60

集合操作だから集合論とか言うの止めてくれないか

**デフォルトの名無しさん** · 2014/10/11(土) 20:16:24.89

SQLは集合論つーより代数論だ。

**デフォルトの名無しさん** · 2014/10/11(土) 20:16:36.33

別に素朴集合論に単純な型を付けたようなもので普通に用は足りるだろ。
公理的集合論だからといって現実的には何かできることが増えるわけじゃないぞ。
単に数学の基礎を議論する時に必要というだけで。

**デフォルトの名無しさん** · 2014/10/11(土) 20:18:28.72

>>482
その程度のものなら既存で腐る程あるだろ、って話を何度ループすれば気が済むんだ？

**デフォルトの名無しさん** · 2014/10/11(土) 22:48:51.28

で、集合論に何を夢見てるんだ？

**デフォルトの名無しさん** · 2014/10/12(日) 00:31:12.35

素朴集合論ってカントールの集合論のことだぞ。
中学生が習うやつじゃないぞ。

**デフォルトの名無しさん** · 2014/10/12(日) 02:13:46.33

カントンが手術したらモテモテになると勘違いしている様>>1

**デフォルトの名無しさん** · 2014/10/12(日) 20:49:20.54

だから「単純な型を付けたようなもの」って言ってるだろ。
その意味がわかってない？

**デフォルトの名無しさん** · 2014/10/12(日) 20:55:04.62

お前が分かってない。

**デフォルトの名無しさん** · 2014/10/12(日) 21:08:23.19

なんとなくだけど、結論を急いで、できないとか意味がないとか言って、一切の建設的な意見を出さず、妨害だけする人って居るよね？

**デフォルトの名無しさん** · 2014/10/12(日) 21:17:15.44

そりゃこの広い世界のどこかにはそういう人も居るかもしれないね

**デフォルトの名無しさん** · 2014/10/12(日) 21:35:02.06

素朴集合論に型を付けたらうまくいくんじゃね？
とやってみたら恐ろしく複雑で不自由になったのがフレーゲのタイプ理論。
その後100年近く塩漬け状態。
それなら集合とクラスの二つだけに分けて、後はあまり強く型付けしなければ、
カントールの楽園から追放されないんじゃね？
というのがツェルメロの公理的集合論。

集合論、集合論と言っている人は、
無限公理や正則性公理を積極的に言語で使うつもりがあるのかな?
↓必要なのはここまでなんじゃないのかな。
http://ja.wikipedia.org/wiki/%E9%9B%86%E5%90%88%E3%81%AE%E4%BB%A3%E6%95%B0%E5%AD%A6

**デフォルトの名無しさん** · 2014/10/12(日) 22:31:37.21

>>489
どのレス？

**デフォルトの名無しさん** · 2014/10/12(日) 22:35:38.76

S Set
T Theory
P Programming

Aはどうしよう。

**デフォルトの名無しさん** · 2014/10/12(日) 22:38:10.76

advanced
application
applied

**デフォルトの名無しさん** · 2014/10/12(日) 22:44:43.09

the set theory applied programming (STAP) language

略してSTAP言語

**デフォルトの名無しさん** · 2014/10/13(月) 00:27:06.12

で、できたの？

**デフォルトの名無しさん** · 2014/10/13(月) 00:34:39.55

200回ぐらい。

**デフォルトの名無しさん** · 2014/10/13(月) 05:17:51.25

>>489
既存研究のサーベイが皆無なバカが悪い