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

1 ：デフォルトの名無しさん：2014/08/10(日) 21:27:16.56 ID:x7G32Sd0.net

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

810 ：１：2015/01/13(火) 23:38:41.86 ID:ld5ZWEPI.net

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

811 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/13(火) 23:39:26.18 ID:gURRjQHf.net

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

812 ：1：2015/01/14(水) 00:05:14.20 ID:upPMt0VH.net

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

813 ：１：2015/01/14(水) 00:09:20.78 ID:upPMt0VH.net

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

814 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/14(水) 19:03:17.31 ID:lWtQJ7uI.net

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

815 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/15(木) 14:58:59.94 ID:OiYOltU9.net

http://katahiromz.bbs.fc2.com

816 ：デフォルトの名無しさん：2015/01/15(木) 18:04:49.36 ID:UYCK2hGt.net

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

817 ：デフォルトの名無しさん：2015/01/15(木) 20:46:59.13 ID:QgJ4DA/V.net

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

818 ：１：2015/01/15(木) 21:04:35.89 ID:RCkerH2f.net

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

819 ：デフォルトの名無しさん：2015/01/15(木) 22:49:41.86 ID:5ppshwSd.net

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

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

820 ：1：2015/01/15(木) 23:03:37.94 ID:RCkerH2f.net

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

821 ：デフォルトの名無しさん：2015/01/16(金) 00:08:32.30 ID:q80wbXpz.net

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

822 ：１：2015/01/16(金) 00:10:36.55 ID:tbQRRWp6.net

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

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

823 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/16(金) 01:05:01.69 ID:IPI8U3lP.net

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

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

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

824 ：１：2015/01/16(金) 18:38:49.28 ID:tbQRRWp6.net

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

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

825 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/16(金) 18:52:49.05 ID:IPI8U3lP.net

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

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

826 ：１：2015/01/16(金) 19:09:16.59 ID:tbQRRWp6.net

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

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

827 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/16(金) 22:32:01.39 ID:IPI8U3lP.net

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

828 ：１：2015/01/16(金) 23:47:30.80 ID:tbQRRWp6.net

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

829 ：１：2015/01/17(土) 00:13:16.15 ID:e9PIZEl5.net

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

830 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/17(土) 01:27:28.08 ID:PPUSm5YO.net

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

831 ：１：2015/01/17(土) 02:12:55.60 ID:e9PIZEl5.net

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

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

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

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

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

832 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/17(土) 02:59:53.32 ID:PPUSm5YO.net

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

833 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/17(土) 03:31:41.14 ID:PPUSm5YO.net

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

834 ：１：2015/01/18(日) 22:30:12.77 ID:Pnbu8M/I.net

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

835 ：１：2015/01/20(火) 23:02:01.33 ID:RE29itzd.net

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

836 ：デフォルトの名無しさん：2015/01/21(水) 01:37:31.40 ID:+/NZ76QF.net

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

837 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/21(水) 08:55:01.51 ID:y20qOxOP.net

n＝1×nを使う

838 ：1：2015/01/21(水) 19:32:48.10 ID:83hEDbKu.net

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

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.

839 ：１：2015/01/21(水) 19:37:49.38 ID:83hEDbKu.net

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

840 ：１：2015/01/21(水) 20:33:19.47 ID:83hEDbKu.net

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

841 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/21(水) 22:08:31.55 ID:OPHJ2hAi.net

>>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.

842 ：１：2015/01/21(水) 22:49:05.70 ID:83hEDbKu.net

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

843 ：片山博文MZ ◆T6xkBnTXz7B0 ：2015/01/23(金) 02:17:55.54 ID:22/uje4h.net

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

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

844 ：デフォルトの名無しさん：2015/10/21(水) 21:08:46.20 ID:qGjQS7QU.net

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

845 ：デフォルトの名無しさん：2015/10/21(水) 21:49:58.99 ID:kanshW5q.net

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

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

846 ：デフォルトの名無しさん：2016/05/01(日) 11:01:21.14 ID:tKi6j9CT.net

匿名通信（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的に分散され、特定のサーバーに依存しません
ｃ

847 ：デフォルトの名無しさん：2018/02/28(水) 18:29:32.35 ID:F8/eMdWm.net

やぁ

848 ：デフォルトの名無しさん：2018/05/23(水) 22:19:44.05 ID:Au5e7VGg.net

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

TQ9W4

849 ：デフォルトの名無しさん：2018/07/04(水) 23:44:36.75 ID:gFgZc5FG.net

6HI

850 ：デフォルトの名無しさん：2018/11/23(金) 11:17:18.34 ID:lDkmAROy.net

>>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

851 ：デフォルトの名無しさん：2018/11/23(金) 11:18:01.12 ID:lDkmAROy.net

sum (x:xs) = x + sum xs

852 ：デフォルトの名無しさん：2018/11/25(日) 12:00:26.30 ID:mrb3Dvz9.net

もう許してやれよ

853 ：デフォルトの名無しさん：2019/06/19(水) 05:01:29.66 ID:tVNS+22r.net

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

854 ：デフォルトの名無しさん：2019/09/20(金) 10:28:23.43 ID:4f4Q+09G.net

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

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

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

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

855 ：デフォルトの名無しさん：2020/01/09(木) 12:03:21.50 ID:Ydnkghao.net

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

856 ：デフォルトの名無しさん：2021/03/30(火) 16:01:29.49 ID:WEbCupCq/

最高か！アプリ開発とアプリマーケティングをノーコードで実現するノーコード開発プラットフォーム
「Applica（アプリカ）」の提供を開始
https://prtimes.jp/main/html/rd/p/000000003.000069846.html
驚愕！SaaS開発をノーコードで実現するノーコード開発プラットフォーム「Jidoca（ジドウカ）」の提供を開始
https://prtimes.jp/main/html/rd/p/000000001.000069846.html
【入門】誰でもアプリを作れる時代が来た。噂の“ノーコード”を徹底解説
https://www.salesforce.com/jp/blog/2021/02/low-code-1-newspicks.html
IT業界を変える可能性を秘める「ノーコード（NoCode）」とは
https://www.mdsol.co.jp/column/column_122_1700.html
【ノーコード】IT業界が根底から変わる、日本人の知らないノーコード開発アプリの衝撃
https://descartes-search.com/media/nocode-app-developement/
急激に広まるノーコード、ローコードをうまく使いこなせ
https://ascii.jp/elem/000/004/039/4039185/
30億円調達の簡単アプリ開発サービス「ヤプリ」が見つけた“鉱脈”
https://signal.diamond.jp/articles/-/13
プログラミング不要でアプリ開発を実現する「Yappli」を提供、ヤプリのIPOサマリー
https://media.startup-db.com/research/yappli-ipo
ノーコードで世界は変わる
https://thebridge.jp/2020/08/nocode-will-change-the-world

857 ：デフォルトの名無しさん：2021/03/30(火) 16:53:31.28 ID:WEbCupCq/

Excelとビジュアルプログラミングが融合したWebアプリ開発ツール「CELF」が、ビジネスパーソン総プログラマ時代を実現
https://japan.zdnet.com/pickup/scsk_201607/35085538/
ビジュアルプログラミング言語を俯瞰する(ScratchからNode-RED、TouchDesignerやIFTTTまで)
https://qiita.com/tomo_makes/items/c193d4fc89e6eb4a245d
ビジュアルプログラミングってなに？〜3タイプ分類でわかるScratchやViscuitの違い
https://tool-zukan.com/column/3752/
教育用プログラミング言語とは？徹底紹介5選｜おすすめビジュアルプログラミング
https://coeteco.jp/articles/10644
ビジュアル・プログラミング
http://web.sfc.keio.ac.jp/~hattori/visual-prog/html4/main.html
義務教育の「残念なプログラミング授業」、現役エンジニアが危惧
https://diamond.jp/articles/-/198744

858 ：デフォルトの名無しさん：2023/08/01(火) 14:12:19.18 ID:GW8b/jIq0

クソ航空機に生活や仕事を妨害されたら‥アプリ『ADS-B Unfiltered Plane Tracker」て゛登録記號を確認，証拠としてスクショも残しつつ
https://jasearch.info/aircraft_hist.html
↑ここて゛検索して所有者(使用者)を特定したら、ググって電話番号を確認、この地球破壊私権侵害強盗殺人テ囗リス├にクレ━ムを入れよう！
例えば，登録記號『JA17AR」は氣候変動させて災害連發させて人を殺して私腹を肥やしてるとっとと津波て゛絶滅すへ゛き「札幌市』だと分かる
最近スマホのパケづまりが酷いか゛航空無線の広大なプラチナ帯域によってネッ├帯域か゛不足してるのが原因，クソ航空関係者に年１Ο０兆圓
課税するとともに帯域を明け渡させよう！言うまでもなく四六時中猥褻がらみて゛逮捕されなか゛ら威力業務妨害ヘリ飛ばしまくって望遠力メラで
女風呂のぞき見しなか゛らグルク゛儿騷音まき散らして住民イライラ犯罪惹起してる税金泥棒クソポリ公ヘリ，特に他県にまて゛大騒音まき散らし
てる警視庁「JA1?MP』など惡質だか゛、テ口政府を徹底非難するとともに、傷害や威力業務妨害として告訴して．私権侵害テロを止めさせよう！

創価学會員は、何百萬人も殺傷して損害を与えて私腹を肥やし続けて逮捕者まて゛出てる世界最悪の殺人腐敗組織公明党を
池田センセ一が□をきけて容認するとか本気で思ってるとしたら侮辱にもほと゛があるそ゛！
https://i.imgur.com/hnli1ga.jpeg

859 ：デフォルトの名無しさん：2024/02/27(火) 13:10:32.62 ID:Xgl6YtAjB

人間の尊厳カ゛ーた゛のと心にもないことをぬけぬけとぬかしていやか゛る岸田異次元増税憲法ガン無視地球破壊覇権主義文雄や
世界最悪の殺人テロ組織公明党強盗殺人の首魁蓄財3億円超の斉藤鉄夫は暴力を続け多くの人に苦しみを与え人間の尊厳を踏みにじれば
住民は妥協し知的能力者も抗議をやめると見込んでいる，しかし知的能カ者もわれわれも諦めない
世界最悪脱炭素拒否テロ國家に送られる化石賞４連続受賞して世界中から非難されなか゛ら憲法13条2５条29条と公然と無視して力による一方的な
現状変更によってクソ航空機倍増．閑静な住宅地から都心まて゛数珠つなぎて゛鉄道の30倍以上もの莫大な温室効果カ゛スまき散らして騷音まみれ
気候変動させて海水温上昇させてかつてない量の水蒸氣発生させて土砂崩れ、洪水、暴風．熱中症にと災害連発させて住民の生活破壞して
静音が生命線の知的産業を壊滅させるなどのクソ航空機による惨劇を止めねばならない、侵略者を打ち負かすため団結するべきだ
気候変動騒音犯罪は処罰され生活を破壞された人たちは賠償され侵略者は皆殺しにされるべきた゛と訴え正義を実現するための行動を起こそう!
(ref.) Ttрs:/／www.сall4.jp／info.phｐ?Τype=items&id=I0000062
тtρs:／/haneda-projｅСТ.jimdofree.com/ , ttｐs：/／flight-routｅ.сom／
ttPs://n-souonhigaisosyoudan.amebaownd.сom／