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

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

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

１ · 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言語ではだめですか