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

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

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

**デフォルトの名無しさん** · 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.

１ · 2015/01/21(水) 19:37:49.38

Coqは一日一時間までにする。
それ以上は自重。

１ · 2015/01/21(水) 20:33:19.47

片山さんの模範解答うｐ希望

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

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

１ · 2015/01/21(水) 22:49:05.70

ふーむ。確かに片山さんのほうが自然な証明ですな。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 02:17:55.54

布教のために数学板でも展開するぞ。

【Coq】コンピューターで証明しよう【コック】･2ch.net
http://wc2014.2ch.net/test/read.cgi/math/1421944863/

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

http://connect4.game-solver.org/?pos=

**デフォルトの名無しさん** · 2015/10/21(水) 21:49:58.99

ほう、4並べのソルバですか。面白い

なぜこのスレなのかは気にしないでおこう
thx

**デフォルトの名無しさん** · 2016/05/01(日) 11:01:21.14

匿名通信（Tor、i2p等）ができるファイル共有ソフトBitComet（ビットコメット）みたいな、
BitTorrentがオープンソースで開発されています

言語は何でも大丈夫だそうなので、P2P書きたい！って人居ませんか？

Covenantの作者（Lyrise）がそういう人と話したいそうなので、よろしければツイートお願いします
https://twitter.com/Lyrise_al

ちなみにオイラはCovenantの完成が待ち遠しいプログラミングできないアスペルガーｗ

The Covenant Project
概要

Covenantは、純粋P2Pのファイル共有ソフトです

目的

インターネットにおける権力による抑圧を排除することが最終的な目標です。そのためにCovenantでは、中央に依存しない、高効率で検索能力の高いファイル共有の機能をユーザーに提供します

特徴

Covenant = Bittorrent + Abstract Network + DHT + (Search = WoT + PoW)

接続は抽象化されているので、I2P, Tor, TCP, Proxy, その他を利用可能です
DHTにはKademlia + コネクションプールを使用します
UPnPによってポートを解放することができますが、Port0でも利用可能です(接続数は少なくなります)
検索リクエスト、アップロード、ダウンロードなどのすべての通信はDHT的に分散され、特定のサーバーに依存しません
ｃ

**デフォルトの名無しさん** · 2018/02/28(水) 18:29:32.35

やぁ

**デフォルトの名無しさん** · 2018/05/23(水) 22:19:44.05

僕の知り合いの知り合いができたパソコン一台でお金持ちになれるやり方
役に立つかもしれません
グーグルで検索するといいかも『ネットで稼ぐ方法　モニアレフヌノ』

TQ9W4

**デフォルトの名無しさん** · 2018/07/04(水) 23:44:36.75

6HI

**デフォルトの名無しさん** · 2018/11/23(金) 11:17:18.34

>>118
Haskellのクイックソートはリスト内包表記使った方が美しい。

qsort [] = []
qsort (x:xs) = small ++ [x] ++ leage
where
small = qsort [a|a <- xs,a <= x]
leage = qsort [a|a <- xs,a > x]

>>1 が求めるのってHaskellやPythonのリスト内包表記だけでプログラミングしたいとか？
SQLやC#のLinqにも通じるけど。

集合論的なのがあれば便利だけど、「だけ」と言うのはプログラミング上もキツイと思うな。

文字数を求める関数

再帰版
length [] = []
length (_:xs) = 1 + length xs

リスト内包表記版
length xs = sum [1 | _ <- xs] ― リスト内包表記で1行になるけど、結局sum関数は必要。(チャレンジしたけど、リスト内包表記だけでsum関数は無理ぽ)

sum [] = 0
sum (x:xs) = x + sum xs

**デフォルトの名無しさん** · 2018/11/23(金) 11:18:01.12

sum (x:xs) = x + sum xs

**デフォルトの名無しさん** · 2018/11/25(日) 12:00:26.30

もう許してやれよ

**デフォルトの名無しさん** · 2019/06/19(水) 05:01:29.66

【出資】松本卓朗人工知能詐欺【注意】
https://rio2016.5ch.net/test/read.cgi/rikei/1560859403/

**デフォルトの名無しさん** · 2019/09/20(金) 10:28:23.43

Haskellじゃないの？
集合とか要素に型、集合にも型名を与えて処理する
Haskellとモナドの動画見てたけど少しだけ理解

計算は集合が状態遷移で形態(形状)変化した結果だと思う
[1 1]->sum->[1]みたいな

モナドの適当な感想
モナドは状態遷移を行う処理手続き関数の中に
バグや矛盾が入り込みにくい小さなプログラム単位を数珠つなぎに連鎖させ
エラーなり問題点の発生場所を明確化する手法な気がした

scalaのモナドは読むの辛いね(慣れ？)

**デフォルトの名無しさん** · 2020/01/09(木) 12:03:21.50

>>1
Z言語ではだめですか