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

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

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

**デフォルトの名無しさん** · 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を偶数と奇数に場合分けする方法がわからんとです。

１ · 2015/01/13(火) 23:04:11.48

even(1+n)にeven(1+n) -> odd nをapplyして odd nにならんのか？
よくわからん。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/13(火) 23:09:34.67

Lemma oS: forall n:nat, even n -> odd (S n).
intros.
apply odd_S.
apply H.
Qed.

１ · 2015/01/13(火) 23:38:41.86

証明済みのLemmaの活用の仕方がわからんです。
applyじゃないの？

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/13(火) 23:39:26.18

replace (even (S n)) with (odd n).
apply even_or_odd.
もう少しだな。

1 · 2015/01/14(水) 00:05:14.20

A=Bを示したかったらA->BかつB->Aで方針あってますか?

１ · 2015/01/14(水) 00:09:20.78

もう寝ます。
また明日よろしくお願いします。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/14(水) 19:03:17.31

聞きたいことがあれば、俺の掲示板に来いよ。待ってるぜ。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/15(木) 14:58:59.94

http://katahiromz.bbs.fc2.com

**デフォルトの名無しさん** · 2015/01/15(木) 18:04:49.36

>>814-815
1がそっちに行ってくれればいいけど。
1はCoqとか本当はどうでもよくて、このスレに書くこと自体が目的になってるだろうから・・・

**デフォルトの名無しさん** · 2015/01/15(木) 20:46:59.13

>>816
雑談はこちらの412に書いてるな。
戻ってくるなよ＞1

１ · 2015/01/15(木) 21:04:35.89

お前らこのスレが伸びちゃ困る理由でもあるのかｗ

**デフォルトの名無しさん** · 2015/01/15(木) 22:49:41.86

>>818
1が「集合論に基づいた言語を作る」話をしないからな。
>>425 >>559 >>655-665

どうせエサをくれるのは片山博文MZだけなんだから、ずっとあっちに行ってろよ。

1 · 2015/01/15(木) 23:03:37.94

このスレはお前らで盛り上げてくれてもかまわないんだぜ？

**デフォルトの名無しさん** · 2015/01/16(金) 00:08:32.30

このスレ見てるの結構楽しい（煽りとかではなくいろんな話が出てくるし）から盛り上がって欲しい

１ · 2015/01/16(金) 00:10:36.55

できたっぽい。
片山さんに教えてもらったページみた。

Require Import Even.

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

elim n.
left.
apply even_O.

intros.
elim H.
right.
apply even_S.
apply odd_S.
apply H0.
left.
apply H0.
Qed.

Coq相当親切なチュートリアルがないと勉強できんわ。
どのタクティク使えばいいのかとかわからんすぎる。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/16(金) 01:05:01.69

>>822
なかなかやるじゃん。

ついでに「片山QZの定理」の証明でもやってみる？

片山QZの定理
http://katahiromz.web.fc2.com/mathai/

１ · 2015/01/16(金) 18:38:49.28

MZとかQZとかって何なの？
別にいいんだけど。

片山QZの定理はなんかえらい難しそうなのでやめとく。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/16(金) 18:52:49.05

QZというのはC/C++宿題スレに生息している人だよ。

そうだな。2n＝n＋nの証明なんかどうかな？楽勝？

１ · 2015/01/16(金) 19:09:16.59

掛け算の定義がどこにあるのかわからん。

証明もいいけどコードの自動生成のほうが面白そうかな～

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/16(金) 22:32:01.39

>>826
英語では、掛け算がmultiplicationで、自然数がnatural numbersだろ？
それを略すればmul,natになるだろ？
SearchAbout mul.
SearchAbout nat.
で検索できるから。

１ · 2015/01/16(金) 23:47:30.80

>>827
結構むずかしい。
仮にできたとしても時間かかると思う。

１ · 2015/01/17(土) 00:13:16.15

ぶっちゃけCoqやってると無限に時間を吸われる可能性がある。
早めに身を引いた方がよさそうかな～とも思う。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/17(土) 01:27:28.08

数学に基づいた言語としてCoqは最適の例かと思われたが、御気に召さないとはこれ如何に。
では、そなたはどのような言語が希望か申し上げてみよ。

１ · 2015/01/17(土) 02:12:55.60

いや～確かにCoq面白いんだけど。
勉強するのに時間かかり過ぎるっていうか
もうちょっと市民権を得て入門書とか充実してからの方がいいかな～と。

証明も紙なら簡単にできることが結構難しかったりで、
実利を得るところまで勉強進めるのがしんどい。
実用までいかなくてただのパズルで終わりそう。

Coq参考になるところは多いと思うんだけどね。

どこまで時間費やすか見極めたほうがよさげ。

片山さんはCoqにどの程度手ごたえ感じてるの？

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/17(土) 02:59:53.32

麿は、この素晴らしきCoqを使えば、不具合のないソフトウェアが作れると見ては、
これをマスターすれば世界征服も夢ではないと、そのような所存でおじゃるよ。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/17(土) 03:31:41.14

Coqと人工知能を組み合わせたら……、金融取引に活かせば……とか楽しい妄想が広がるでおじゃる。

１ · 2015/01/18(日) 22:30:12.77

人工知能といえばdeep learningとかいうのが流行らしいんだが。

１ · 2015/01/20(火) 23:02:01.33

2n=n+nはomegaで一発っぽい。
omegaなしだとどうやるかわからん。

**デフォルトの名無しさん** · 2015/01/21(水) 01:37:31.40

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

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/21(水) 08:55:01.51

n＝1×nを使う

1 · 2015/01/21(水) 19:32:48.10

途中よけいなことしてるかもだができたっぽい。

Require Import Arith.
Theorem t:forall n:nat,2*n=n+n.
intros.
replace (2*n) with (n*(S 1)).
symmetry.
replace (n+n) with (n*1+n).
apply mult_n_Sm.
replace (n*1) with (1*n).
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
apply mult_comm.
apply mult_comm.
Qed.