X
集合論に基づいた言語を作りたい
■ このスレッドは過去ログ倉庫に格納されています
0001デフォルトの名無しさん垢版2014/08/10(日) 21:27:16.56ID:x7G32Sd0
計算機科学の基礎は集合論であるという。
ならば、集合論に基づいた言語を作れば美しい言語になるのでは？
そんな発想から徹底的に集合論的思想で言語仕様を考えるスレです。
0806片山博文MZ ◆T6xkBnTXz7B0 垢版2015/01/13(火) 21:52:38.35ID:gURRjQHf
ヒント。
Require Import Even.
Lemma eSr: forall n:nat, even (1 + n) -> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.
0807１垢版2015/01/13(火) 22:46:33.61ID:ld5ZWEPI
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を偶数と奇数に場合分けする方法がわからんとです。
0808１垢版2015/01/13(火) 23:04:11.48ID:ld5ZWEPI
even(1+n)にeven(1+n) -> odd nをapplyして odd nにならんのか？
よくわからん。
0810１垢版2015/01/13(火) 23:38:41.86ID:ld5ZWEPI
証明済みのLemmaの活用の仕方がわからんです。
applyじゃないの？
08121垢版2015/01/14(水) 00:05:14.20ID:upPMt0VH
A=Bを示したかったらA->BかつB->Aで方針あってますか?
0813１垢版2015/01/14(水) 00:09:20.78ID:upPMt0VH
もう寝ます。
また明日よろしくお願いします。
0816デフォルトの名無しさん垢版2015/01/15(木) 18:04:49.36ID:UYCK2hGt
>>814-815
1がそっちに行ってくれればいいけど。
1はCoqとか本当はどうでもよくて、このスレに書くこと自体が目的になってるだろうから・・・
0818１垢版2015/01/15(木) 21:04:35.89ID:RCkerH2f
お前らこのスレが伸びちゃ困る理由でもあるのかｗ
08201垢版2015/01/15(木) 23:03:37.94ID:RCkerH2f
このスレはお前らで盛り上げてくれてもかまわないんだぜ？
0821デフォルトの名無しさん垢版2015/01/16(金) 00:08:32.30ID:q80wbXpz
このスレ見てるの結構楽しい（煽りとかではなくいろんな話が出てくるし）から盛り上がって欲しい
0822１垢版2015/01/16(金) 00:10:36.55ID:tbQRRWp6
できたっぽい。
片山さんに教えてもらったページみた。

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相当親切なチュートリアルがないと勉強できんわ。
どのタクティク使えばいいのかとかわからんすぎる。
0824１垢版2015/01/16(金) 18:38:49.28ID:tbQRRWp6
MZとかQZとかって何なの？
別にいいんだけど。

片山QZの定理はなんかえらい難しそうなのでやめとく。
0825片山博文MZ ◆T6xkBnTXz7B0 垢版2015/01/16(金) 18:52:49.05ID:IPI8U3lP
QZというのはC/C++宿題スレに生息している人だよ。

そうだな。2n＝n＋nの証明なんかどうかな？ 楽勝？
0826１垢版2015/01/16(金) 19:09:16.59ID:tbQRRWp6
掛け算の定義がどこにあるのかわからん。

証明もいいけどコードの自動生成のほうが面白そうかな〜
0827片山博文MZ ◆T6xkBnTXz7B0 垢版2015/01/16(金) 22:32:01.39ID:IPI8U3lP
>>826
英語では、掛け算がmultiplicationで、自然数がnatural numbersだろ？
それを略すればmul,natになるだろ？
SearchAbout mul.
SearchAbout nat.
で検索できるから。
0828１垢版2015/01/16(金) 23:47:30.80ID:tbQRRWp6
>>827
結構むずかしい。
仮にできたとしても時間かかると思う。
0829１垢版2015/01/17(土) 00:13:16.15ID:e9PIZEl5
ぶっちゃけCoqやってると無限に時間を吸われる可能性がある。
早めに身を引いた方がよさそうかな〜とも思う。
0830片山博文MZ ◆T6xkBnTXz7B0 垢版2015/01/17(土) 01:27:28.08ID:PPUSm5YO
数学に基づいた言語としてCoqは最適の例かと思われたが、御気に召さないとはこれ如何に。
では、そなたはどのような言語が希望か申し上げてみよ。
0831１垢版2015/01/17(土) 02:12:55.60ID:e9PIZEl5
いや〜確かにCoq面白いんだけど。
勉強するのに時間かかり過ぎるっていうか
もうちょっと市民権を得て入門書とか充実してからの方がいいかな〜と。

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

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

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

片山さんはCoqにどの程度手ごたえ感じてるの？
0832片山博文MZ ◆T6xkBnTXz7B0 垢版2015/01/17(土) 02:59:53.32ID:PPUSm5YO
麿は、この素晴らしきCoqを使えば、不具合のないソフトウェアが作れると見ては、
これをマスターすれば世界征服も夢ではないと、そのような所存でおじゃるよ。
0833片山博文MZ ◆T6xkBnTXz7B0 垢版2015/01/17(土) 03:31:41.14ID:PPUSm5YO
Coqと人工知能を組み合わせたら……、金融取引に活かせば……とか楽しい妄想が広がるでおじゃる。
0834１垢版2015/01/18(日) 22:30:12.77ID:Pnbu8M/I
人工知能といえばdeep learningとかいうのが流行らしいんだが。
0835１垢版2015/01/20(火) 23:02:01.33ID:RE29itzd
2n=n+nはomegaで一発っぽい。
omegaなしだとどうやるかわからん。
08381垢版2015/01/21(水) 19:32:48.10ID:83hEDbKu
途中よけいなことしてるかもだができたっぽい。

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.
0839１垢版2015/01/21(水) 19:37:49.38ID:83hEDbKu
Coqは一日一時間までにする。
それ以上は自重。
0840１垢版2015/01/21(水) 20:33:19.47ID:83hEDbKu
片山さんの模範解答うｐ希望
0841片山博文MZ ◆T6xkBnTXz7B0 垢版2015/01/21(水) 22:08:31.55ID:OPHJ2hAi
>>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.
0842１垢版2015/01/21(水) 22:49:05.70ID:83hEDbKu
ふーむ。確かに片山さんのほうが自然な証明ですな。
0846デフォルトの名無しさん垢版2016/05/01(日) 11:01:21.14ID:tKi6j9CT
匿名通信（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的に分散され、特定のサーバーに依存しません
ｃ
0848デフォルトの名無しさん垢版2018/05/23(水) 22:19:44.05ID:Au5e7VGg
僕の知り合いの知り合いができたパソコン一台でお金持ちになれるやり方
役に立つかもしれません
グーグルで検索するといいかも『ネットで稼ぐ方法　モニアレフヌノ』

TQ9W4
0849デフォルトの名無しさん垢版2018/07/04(水) 23:44:36.75ID:gFgZc5FG
6HI
0850デフォルトの名無しさん垢版2018/11/23(金) 11:17:18.34ID:lDkmAROy
>>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
0851デフォルトの名無しさん垢版2018/11/23(金) 11:18:01.12ID:lDkmAROy
sum (x:xs) = x + sum xs
0852デフォルトの名無しさん垢版2018/11/25(日) 12:00:26.30ID:mrb3Dvz9
もう許してやれよ
0854デフォルトの名無しさん垢版2019/09/20(金) 10:28:23.43ID:4f4Q+09G
Haskellじゃないの？
集合とか要素に型、集合にも型名を与えて処理する
Haskellとモナドの動画見てたけど少しだけ理解

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

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

scalaのモナドは読むの辛いね(慣れ？)
0855デフォルトの名無しさん垢版2020/01/09(木) 12:03:21.50ID:Ydnkghao
>>1
Z言語ではだめですか
■ このスレッドは過去ログ倉庫に格納されています
ニューススポーツなんでも実況