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

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

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

**デフォルトの名無しさん** · 2014/11/09(日) 16:46:55.86

1は何かものを作れる人間じゃないから。

１ · 2014/11/09(日) 18:17:59.58

>>707
んーどうだろうな。
俺もスレたてた時はすべてを集合で表せば数学的にうまくいくんじゃね？とか思ってたんだけど、
やっぱリストはリスト、タプルはタプルなんだよな。
connect4も無理に集合的に扱わないで手続型で扱った方が自然かもしれないんだよな～
ぶっちゃけ、集合にこだわる意味が根底から揺らいでるｗ
数学の基礎的な部分が集合論でできてるってのはそうなんだろうけど、
応用問題解くときに些末な問題に煩わされたくないよね？

まあ、集合論でうまくいきそうな問題⇔教科書の章末問題かなぁとか思ってたんだけどさ。
その辺はあんまり整理できてない。

**デフォルトの名無しさん** · 2014/11/09(日) 19:17:53.75

リストもタプルも集合論の枠組み内で普通に扱えるのだが、
もういいや、1に何かを期待するのはやめた。

**デフォルトの名無しさん** · 2014/11/09(日) 19:30:26.31

そろそろループ再開ですか？

**片山博文MZ次期CEO** ◆T6xkBnTXz7B0 · 2014/11/09(日) 19:44:15.77

算術演算＋－×÷！／√
括弧（）［］
等号不等号＝≠＜＞≦≧≒≪≫
無限大∞
集合∈∋⊆⊇⊂⊃∪∩｛｜｝＃
論理：∧∨￢⇒⇔∀∃→∴∵
パーセント％
その他の記号±≡…；？

**デフォルトの名無しさん** · 2014/11/09(日) 20:00:10.30

1に餌を与えないでください。
>>425 >>559 >>655-665

**片山博文MZ次期CEO** ◆T6xkBnTXz7B0 · 2014/11/09(日) 20:28:33.70

俺の研究内容が似ているので燃料投下する。国の生活保護と同様に、たとえ悪魔にもエサを与えよう。

**デフォルトの名無しさん** · 2014/11/09(日) 21:17:29.34

1「悪魔の餌クレクレ」

１ · 2014/11/10(月) 21:45:18.40

試しにRubyでconnect4書いてみた。
http://www.age2.tv/rd05/src/up5560.txt.html

行数的にはhaskellのほうが短いくらいなんだが^^;
オフサイドルールのせいかな？

**デフォルトの名無しさん** · 2014/11/11(火) 04:23:27.89

>>716
スレ違いだバカ

**デフォルトの名無しさん** · 2014/11/11(火) 16:25:56.08

スレタイでHaskellで良いじゃんと思ってスレ開いたら１が馬鹿すぎてスレをそっと閉じることにした

１ · 2014/11/17(月) 21:47:20.82

とりあえず、次の宿題は圏論かな～？

１ · 2014/11/17(月) 23:26:02.06

とりあえず、ここ読んだけど。。。

http://ja.wikibooks.org/wiki/Haskell/%E5%9C%8F%E8%AB%96

ぃみゎかんなぃ。。

もぅﾏﾁﾞ無理。。

ﾘｽｶしょ・・・

ようするにdoが使いたいだけ？

**デフォルトの名無しさん** · 2014/11/18(火) 00:04:28.78

>>720
Haskellスレでやれ。
Haskellに詳しい人はそっちのほうが多いはずだ。

関数型プログラミング言語Haskell Part26
http://peace.2ch.net/test/read.cgi/tech/1406436392/

**デフォルトの名無しさん** · 2014/11/18(火) 00:07:08.02

1に餌を与えないでください。
>>425 >>559 >>655-665

１ · 2014/11/18(火) 21:56:19.27

http://d.hatena.ne.jp/Lost_dog/20111211/1323616949
ここも読んでみたけどやっぱわからん。
というか、読んでも目が滑る。
だれか圏論のいい入門textプリーズ

**デフォルトの名無しさん** · 2014/11/19(水) 19:50:12.10

とりあえず『圏論の基礎』でも読んでみたら？

１ · 2014/11/19(水) 19:56:54.80

http://www.amazon.co.jp/dp/4621063243
これ？
まあ本屋いってみてあったら立ち読みしてみるわ。

１ · 2014/11/26(水) 20:02:22.17

圏論の基礎買ったけど早くも積読ｗ

**デフォルトの名無しさん** · 2014/11/29(土) 18:24:47.22

>>701 の話だけど、ドコモで prolog が動いてる的な記事をなんかで読んだことがある

１ · 2014/11/30(日) 19:47:48.77

http://iiyu.asablo.jp/blog/2014/07/28/7400231
これか。
コード量１０分の一は確かにすごい。
しかし2370万行とか正気の沙汰じゃないな。

**デフォルトの名無しさん** · 2014/11/30(日) 22:28:37.23

Prolog で書くと「コード量１０分の一」となる例には、他にも型推論があるね
以下のblog記事では、単純な型推論をPrologで記述している
・Prolog で型チェック：Rainy Day Codings：So-net blog
　http://rainyday.blog.so-net.ne.jp/2008-06-16

自分の知る範囲では、世界で最も簡潔な型推論の実装コードだね
これも、もし(型システムという)形式的なルールが定義されていれば、
それを直接的に表現できるという Prolog の特徴が活かされている
Haskell でもこんな芸当はできない

**デフォルトの名無しさん** · 2014/12/01(月) 15:16:30.87

おおっと、Haskell信者に対して挑発だ～！

**デフォルトの名無しさん** · 2014/12/01(月) 15:51:58.42

別にユニフィケーションがどっち方向にも働く、というのはPrologの特性だし、
Haskellにそんなものあっても困るだけだし。

１ · 2014/12/01(月) 19:25:13.06

>>729
ふーむ。Rubyだとどうなるかな～。
ヨクワカラヌ。

**デフォルトの名無しさん** · 2014/12/01(月) 20:27:28.82

Prologのシンボル使ったユニフィケーションを実装するのは
Rubyに限らず手続き型言語ではライブラリ頼りでやらんと面倒い
むしろそれに特化され過ぎて、手続き的な書き方が面倒いって言語がProlog

**デフォルトの名無しさん** · 2014/12/01(月) 22:36:56.45

そういったものをなんでもまぜこぜできるからLispは偉い、というのが
竹内先生@NUEの主張だったなw

**デフォルトの名無しさん** · 2014/12/01(月) 23:52:04.88

1に餌を与えないでください。
>>425 >>559 >>655-665

1は推論や数式処理を扱うのは面倒くさいと思っている。
>>574-576

**デフォルトの名無しさん** · 2014/12/02(火) 00:14:21.85

集合論だと逐次処理やりにくいしな
SQLとも違うみたいだし

**デフォルトの名無しさん** · 2014/12/03(水) 15:47:19.25

集合論だと、逐次処理は処理系の中でやる。
プログラムにはmapやらfilterやらが出てきて、逐次処理は隠蔽されるのでは？

それを考えると、１がlispで満足できないのが不思議でならない。

まぁ、文字通り「何も」考えていないのだろうな。

１ · 2014/12/03(水) 19:55:52.44

lispってそんないいかなぁ。
ちょっとやったことあるけど、インデントつけても括弧の対応がすぐわかんなくなるんだが。
コード読みにくいったらありゃしない。

**デフォルトの名無しさん** · 2014/12/03(水) 20:36:17.67

>>738
ちょっとやってみただけで慣れようともせずケチつける。
>>700 >>701 >>705 >>706

**デフォルトの名無しさん** · 2014/12/03(水) 21:18:09.35

>>734
S式を使っているからうまく混ぜられる、S式こそLisp最大の特長、とかいう主張だったな。

１ · 2014/12/03(水) 22:35:36.35

>>740
詳しく

**デフォルトの名無しさん** · 2014/12/03(水) 23:15:45.16

ほげ言語のパラドックスでも読んどけ

**デフォルトの名無しさん** · 2014/12/04(木) 01:08:18.94

集合に順序があるのはむしろベクトルかタプルに見える

集合論って考えは好きだけどソートみたいな逐次処理でよく使うものはどうなるんだろうか
並列処理的なこと考えてるひとがいるみたいなんでそれに乗っかると
並列処理ならクイックソートよりマージソートのほうが速そうだがそれが集合論かと言われるとちょっと困る

でもソートが本来のやりたいことではなくてソートしたデータにまた何らかの処理をする要求のほうが多い気がするんでどうでもいいか
2分探索なり逐次処理の環境で考えだされたアルゴリズムはほとんど使えない気がするんでまた誰かが良さそうな手順を考えださないとな

**デフォルトの名無しさん** · 2014/12/05(金) 09:26:36.60

数学できる人間に見られたいクズが集まるスレ

**デフォルトの名無しさん** · 2014/12/05(金) 11:54:06.72

自己紹介か？

１ · 2014/12/05(金) 20:20:24.20

とりあえず、圏論からは戦術的転進するか。
別のネタを探そう。

**デフォルトの名無しさん** · 2014/12/05(金) 20:55:48.99

1に餌を与えないでください。
>>425 >>559 >>655-665

**デフォルトの名無しさん** · 2014/12/05(金) 23:22:33.28

しかしまあスレタイ通りにはなかなかいってないけど総合的には良スレっぽい

**デフォルトの名無しさん** · 2014/12/06(土) 01:07:31.28

>>746
圏論を勉強する気など最初からなくて、ネタのつもりだったわけだ。
圏論以外に何をもってきても同じだろうな。

**デフォルトの名無しさん** · 2014/12/06(土) 10:37:54.51

lisp の括弧は rainbow-parentheses 的なの入れるとマシになる

**デフォルトの名無しさん** · 2014/12/06(土) 18:03:11.24

lispで区切りに()だけ使うんじゃなくて集合を表す時は{}使うとかどうなの？
集合は{

１ · 2014/12/06(土) 18:04:03.49

途中で書き込んじゃった。
集合は{}で表すってイメージあるんだけど。

**デフォルトの名無しさん** · 2014/12/06(土) 18:56:15.26

clojureは#{}が集合のリテラルとしてある
他のlispでもリードマクロかけばそういうことはできる
是非についてなら。その表記が存在することが対象のプログラミングに有効ならあり、そうでなきゃなし

１ · 2014/12/06(土) 18:59:55.68

ほほう。
clojure検討してみる価値あり？

**デフォルトの名無しさん** · 2014/12/06(土) 19:20:33.09

まあlisp系はマクロ書けば簡単に構文拡張できるから、新しい言語を試行錯誤したいなら最適ではあるよ

**デフォルトの名無しさん** · 2014/12/06(土) 19:20:42.39

RubyとかJavaにもSetオブジェクトはあるし、リテラルの有無はソースコードの見た目の問題で、
たいして重要じゃない。

**デフォルトの名無しさん** · 2014/12/06(土) 19:28:14.31

マッチョすぎﾜﾛﾀ
数値や文字列リテラルのない言語でも頑張ってくれそう

１ · 2014/12/06(土) 19:49:14.64

リテラルの有無は結構気になるな、俺は。
Rubyの配列やマップのリテラルは気に入ってる。

１ · 2014/12/06(土) 19:51:57.69

clojureってjavaなのか。
クラスパスとかあんまわかってないんだよな～じつは

**デフォルトの名無しさん** · 2014/12/06(土) 20:40:46.96

>>748
VIPやシベリアだったらな。

１ · 2014/12/06(土) 21:05:36.24

パッと見common lispよりclojureのほうがオサレにみえる。
あんまりcommon lisp知らんけど。

**デフォルトの名無しさん** · 2014/12/06(土) 21:16:11.69

なんでもいいから手を動かせ

１ · 2014/12/07(日) 00:04:16.45

OO言語だとobj.method(x)って書くけどlisp系だと(method obj x)って書くじゃん？
OO言語になれてるからかこの順番の違いが結構イラつく。

**デフォルトの名無しさん** · 2014/12/07(日) 00:11:32.48

ほんとこの１は駄目だなw

**デフォルトの名無しさん** · 2014/12/07(日) 01:41:10.92

lispでC風メソッド呼び出し構文開発したってのをどっかのブログでみたな

**デフォルトの名無しさん** · 2014/12/07(日) 02:32:50.17

リテラルでいろいろ指定できるのは便利だけどな
Clojureだと
{key1 obj1 , key2 obj2}でmap
#{obj1 obj2 obj3} でset
[obj1 obj2 obj3] でvector
'(obj1 obj2 obj3) でlist
地味にsetがありがたかったり(他の言語だとsetのリテラル滅多に無い)

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

>>726
圏論の和書として定評があり再版が望まれているのは
http://www.amazon.co.jp/dp/4837504574
amazon 価格がすべてを物語っている

１ · 2014/12/07(日) 17:19:43.84

いつものようにclojureでconnect4書こうと思ったが、
>>763のことを差し引いても想像以上にモチベーション上がんない。
何のせいだ？
パッと見clojure良さそうに見えるのに。
Prologのときも苦戦したがモチベーションは保てた。

**デフォルトの名無しさん** · 2014/12/07(日) 18:06:31.44

>>768
このスレでは集合論に基づいた言語と関係ない話題はルール違反です。

**デフォルトの名無しさん** · 2014/12/07(日) 19:50:11.74

>>768
今度は「なぜか分からないけどモチベーションを保てない」かw

>>425 >>559 >>655-665

**デフォルトの名無しさん** · 2014/12/08(月) 04:17:29.43

>>768
モチベーションを保てないってことだから続かないと思うけど
続けるならClojureスレに行け

【Lisp】プログラミング言語 Clojure #3【JVM】
http://peace.2ch.net/test/read.cgi/tech/1380333808/

１ · 2014/12/09(火) 23:17:28.28

リアルが忙しくなりそうです。
しばらくこれなくなるかもだが、俺が留守の間おまえらでこのスレを盛り上げてくれよな。
よろしく。

**デフォルトの名無しさん** · 2014/12/10(水) 21:31:22.32

削除依頼していけよ

１ · 2014/12/26(金) 19:46:13.23

仕事納めだよ。
しかし見事にレスがついてないな。
お前らで盛り上げてくれていいのに。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/03(土) 12:40:55.68

>>1さんよ、

Coqという言語を使えば、集合論を含む数学の証明や、プログラムの性質や品質保証ができるらしいぞ。
やってみないか？

**デフォルトの名無しさん** · 2015/01/03(土) 14:07:47.18

>>775
>>713-714

1 · 2015/01/03(土) 18:31:19.39

とりあえず片山さんがCoqで一番成功してると思った例題を教えて
それで判断するわ。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/03(土) 19:06:58.41

俺もCoqについては初心者だが、数学、グラフ理論の超難しい問題
「四色問題」の証明がCoqでできたらしい。

1 · 2015/01/03(土) 20:02:04.73

手続き型言語とかに比べて完結に実装できるってこと？面白そうではある

１ · 2015/01/03(土) 20:38:21.69

ID違うと思うけど１です。
簡潔に実装できるんじゃなくて、
実装はHaskellとかでやって、その正しさをCoqで保証するの？
よくわからん。

１ · 2015/01/03(土) 21:16:03.70

Coq単体で動くのか。
prologに近いのか？
ぶっちゃけかなりむずいなこれは。

１ · 2015/01/03(土) 22:17:48.00

わからんということがわかった。
底なし沼みたいな感じやなこれ。

**デフォルトの名無しさん** · 2015/01/03(土) 23:44:50.02

今回のクレクレ・ループは終わりかな。

>>425 >>559 >>655-665

1 · 2015/01/04(日) 13:03:03.07

片山さんはCoqどれくらい書けるの？
例えばド、モルガンの証明とか書けるの？

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/04(日) 21:15:57.30

>>784
TutorialのPDFをコンビニで2in1pageで両面印刷して研究し始めたとこ。
数学と論理学と英語とプログラミングの知識が要求される地獄山だな。

１ · 2015/01/04(日) 21:40:34.76

>>785
そのチュートリアルのURLくだしあ。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/04(日) 21:45:09.09

>>786
「Coq tutorial PDF」で検索

**デフォルトの名無しさん** · 2015/01/04(日) 21:59:00.42

https://coq.inria.fr/distrib/current/files/Tutorial.pdf
これ？
結構分量ありますね。

１ · 2015/01/06(火) 00:03:50.53

Coqで任意の自然数nに対してn*(n+1)が偶数であることを証明しようとしたがどうしてもできない。
だれかHELP.

１ · 2015/01/06(火) 00:34:25.70

定義はこれで。
Theorem t:
forall (n:nat),exists m , (n*(n+1) = 2 * m).

**デフォルトの名無しさん** · 2015/01/06(火) 05:55:25.49

偶数+1は奇数
奇数+1は偶数
遇数*奇数も奇数*遇数も遇数
自然数は奇数か偶数かどちらかである

１ · 2015/01/06(火) 21:04:14.92

「nが奇数ならn+1は偶数」を証明しようとして詰まってる。

Require Import Even.

Lemma l:
forall (n : nat), odd n -> even (n+1).

intros.

induction n.

simpl.

apply even_S.

これでodd 0とかいうのが出てくるけど、ここからどうしていいかわからない。

１ · 2015/01/06(火) 21:10:59.52

「自然数nに対してn*(n+1)が偶数である」
本題のこっちはここまで進んだ。

Require Import Even.

Theorem t:
forall (n:nat), even (n*(n+1)).

intros.

apply even_mult_aux.

１ · 2015/01/06(火) 23:17:17.43

Coq難しすぎんよ～
もう寝る。

１ · 2015/01/07(水) 19:22:04.95

http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt6.html
このページによるとforall (P : Prop), P \/ ~ Pは証明できなんだそうだ。
forall (n:nat), even (n*(n+1)).も証明できないのかもしれないな。

**デフォルトの名無しさん** · 2015/01/07(水) 20:14:30.38

1に餌を与えないでください。
>>425 >>559 >>655-665

1 · 2015/01/07(水) 21:02:58.84

odd 0 -> Falseは証明できたっぽい。
これをどう活用すればいいのかわからない。

Lemma l2:
odd 0 -> False.

apply not_even_and_odd.

apply even_O.

**デフォルトの名無しさん** · 2015/01/08(木) 15:50:20.90

**デフォルトの名無しさん** · 2015/01/08(木) 18:29:26.11

**デフォルトの名無しさん** · 2015/01/08(木) 19:09:01.13

１ · 2015/01/08(木) 20:07:08.21

ハルヒか？

１ · 2015/01/08(木) 22:27:11.24

そもそもodd n -> even (S n)って定義そのものなんだよなぁ。

1 · 2015/01/11(日) 19:52:52.15

ギブアップ。
だれか正解しってたら教えて。

1 · 2015/01/13(火) 18:35:43.03

片山さん答え知ってたら教えて

**デフォルトの名無しさん** · 2015/01/13(火) 20:23:10.10

http://peace.2ch.net/test/read.cgi/tech/1419929875/23
> 23 名前：片山博文MZ ◆T6xkBnTXz7B0 [sage]： 2015/01/13(火) 18:53:35.00 ID:gURRjQHf
> 私はお下品

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/13(火) 21:52:38.35

ヒント。
Require Import Even.
Lemma eSr: forall n:nat, even (1 + n) -> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.

１ · 2015/01/13(火) 22:46:33.61

Lemma l : forall (n:nat), even (1+n)-> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.
apply odd_S.
apply even_O.
Qed.
こう？

nを偶数と奇数に場合分けする方法がわからんとです。