[過去ﾛｸﾞ] 「数学」をプログラミングするには (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
860: 01/16(木)23:35 ID:N/7GMQUm(1) AAS
ところがどっこい
型注釈無しでは型推論ができない、あるいはエラーにすべきか型チェッカが判定できないケースが存在する
まず簡単なのは、ユニオン型だ
f:: () -> Int | Str
みたいな関数は注釈なしでは、ふたつの箇所で異なる型を返してるのが間違いなのかどうか型チェッカには判定できない
パラメータ多相を使う高階関数も型推論が困難だ
map :: (a -> b) -> [a] -> [b]
省10
861: 01/17(金)04:10 ID:VwDpqJJw(1) AAS
なんかグダグダ言ってるけどそれ形式論理なしでできるよね
この話の発端は形式論理が役に立たないってことであって，型が役に立たないって話じゃないよ
862: 01/17(金)06:49 ID:b1HMrou3(1) AAS
単純に、お前の話に誰も興味ないから話題が変わっただけでは
863: 01/17(金)09:10 ID:qO2eRSGs(1) AAS
ocamlなんかは型推論の健全性と完全性を備えているから
どんな式でも型がつくし、型エラーがでなければ正しいプログラムになるというのが保証されてる
健全性と完全性をどちらか捨てるとしたら完全性なので、そういう言語は型注釈が必要になる
864: 01/17(金)16:31 ID:tFlne/Xr(1) AAS
まぁ形式論理も時相論理もプログラミングには何の恩恵もないわな
865(2): 01/17(金)16:59 ID:GO6/DX25(1) AAS
CSは数学を一部利用するが
数学はCSなんて知らんがな状態
866(1): 01/17(金)18:01 ID:7aS9Z/2O(1) AAS
学問にコンプレックス持ってる人って、みっともないね。
867: 01/17(金)20:14 ID:b0CV3tPB(1) AAS
>>857
パラメータ多相のジェネリックな型は特に制約を指定しなければ任意の型がOK何でもありだけど
何の型でもありということは使える範囲も極めて狭いというか
言語によってはprintすることすら任意の型が可能派と必ずしも可能とは限らない派もあり曖昧で
何らかの制約を指定しないと何の処理もできないためその型の値をそのまま返すことしかできなくなってしまう
つまりジェネリック型パラメータに対する制約記述がカギとなる
868(2): 01/18(土)08:09 ID:eX+b185R(1) AAS
>>866
多分コンプレックスとかじゃなくて無駄なものを持ち込まずにシンプルにしておきたいってだけじゃない
869(1): 01/18(土)08:45 ID:BE7PGd83(1) AAS
>>865 数学が専門の人がどんどんCSに入ってきて内容が高度化してるって聞いたぞ俺は
870: 01/18(土)10:15 ID:ERaUWL8N(1) AAS
シンプレックスでコンプレックス
871(1): 01/18(土)11:19 ID:7Jaib8zo(1) AAS
なんでコンプレックスの話が出て来てるのかさっぱり判らん
>>869
それこそ >>865 の説を補強してるだけじゃないの
872: 01/18(土)11:57 ID:xEXW43By(1) AAS
>>868
イミフ
873(1): 01/18(土)12:09 ID:pstj5VhN(1/2) AAS
>>868
数学やCSを持ち込んで対象が複雑になると思ってるのは、
自分が理解できないものにコンプレックス持ってるからだよ
理論を作って対象が複雑になることはあり得ない
874: 01/18(土)12:14 ID:pstj5VhN(2/2) AAS
>>873
一筆書きして最初の場所に戻ってこられるか、は複雑な問題
グラフのすべての頂点から出ている辺の数が偶数、というのは単純な問題
グラフ理論を持ち込んで問題が複雑になったというのは、
頂点・辺・偶数・奇数などの概念が理解できないから
それは数学に対するコンプレックスにほかならない
875: 01/18(土)12:39 ID:84F6tYk8(1) AAS
>>871 P=NP予想とかCSの問題も数学で扱われてるんだから知らんがな状態ではないと思う
876(1): 01/18(土)15:06 ID:2/LPmLwt(1) AAS
プログラミングに必要な数学は数値計算で使う数学くらいか？
微積と線形
圏論がプログラミングで無意味なのは誰でもわかるか
877: 01/18(土)15:34 ID:28NAL8Fg(1) AAS
>>876
プログラミングと数学を分けてる時点で、Qiitaのブログのサンプルコピペしてる雑魚と同レベル
878: 01/18(土)15:41 ID:Zj1ghav+(1) AAS
反論になってないなぁ
879: 01/18(土)16:26 ID:xuSYONRy(1) AAS
プログラミングに数学はいくらでも使うことができる
プログラミングに使う数学とか言ってんのは、ただ単に自分が数学を学びたくないだけ
880: 01/19(日)12:35 ID:fNMlPpUq(1) AAS
Felleisen 30年研究して「プログラミングには型が必要なことがわかった」←これ好き
881(1): 01/20(月)01:24 ID:8nHIoBfi(1) AAS
型＝命題
項＝証明
この対応は、通常のプログラミングでも同様
そう思えないってことは、型の使い方が大雑把すぎるってこと
882: 01/20(月)06:41 ID:qtJTpWnY(1) AAS
>>881
お前のソースコード見せてくれよ
どんだけ立派なのか拝ませてくれ
883: 01/20(月)08:41 ID:jEcxLOMX(1) AAS
立派とは？
884: 01/20(月)08:45 ID:VdwKz6kz(1) AAS
int i=10;
char c='a';
printf("%d\n",i+c);
こんなのがかけるC++ではカリーハワード同型対応なりたたなさそう
885: 01/20(月)09:06 ID:3GFrNXKp(1) AAS
C/C++の型付けは、メモリをなんぼ確保するかの目印でしかないからな
886: 01/23(木)23:15 ID:gkeqtoks(1) AAS
Rustの型はトレイト属性があって
マルチスレッドでも同期が保証される型など
抽象度の高い表現が型システムで扱えるようになってるね
それによりデータ競合が起きないことを型システムで保証してしまってるところが凄いと思った
887(1): 01/24(金)08:08 ID:xJrwwu40(1) AAS
その代わりにmany shared XOR one mutableのキツいルールがあるけどな。
888: 01/24(金)08:08 ID:wJVzGCxN(1/2) AAS
自力で証明するよりも他者の言質を取るというか契約が成立することにより安全が保証される
という思考に人類は依存しすぎている
半導体は自作できないかもしれないが数学は紙媒体でもできる
889: 01/24(金)10:45 ID:QSEbyU6x(1/2) AAS
正直、Rustに心酔してる奴って、程度が低すぎ・・・
PythonやC#みたいなオモチャと比べたら、たしかにRustはマトモだ
だが、しょせんはまだ従来型のプログラミング言語
人間の思考ほどの表現力は無い
890: 01/24(金)10:51 ID:QSEbyU6x(2/2) AAS
言っちゃ悪いが、人間の知能は平等ではない
ある人にとってはRustは自分の思考よりも高機能だから、Rustに引き上げてもらえる
しかし、ある人にとってはRustを書くことは、Rustの書き方に思考を制限することになる
891(1): 01/24(金)11:18 ID:YFrK1zgU(1) AAS
ある人は数論幾何学や場の量子論などがわかるが、ある人は中学校の連立方程式くらいしかわからない
連立方程式が世界で一番高度な学問と感じる人にとって、プログラミン言語はまるで魔法のようなのかも知れない
が、数論幾何の水準の人にはプログラミング言語は耐え難いほど低水準だ
892: 01/24(金)11:22 ID:wJVzGCxN(2/2) AAS
振舞いを自動化しろと言われるのと判断は人間の責任っていうのは
振舞いと判断を区別すれば矛盾しないんだけど
「証明する」というのは振舞いか判断かさっぱり分からんから矛盾だという批判がある
893: 01/24(金)22:28 ID:TVTggs3s(1) AAS
>>887
single writer XOR multiple readers はデータ参照の競合バグを防ぐために役立つルール
これを守ると参照競合によるバグを防げるだけでなく
プログラムのスパゲッティ化を防ぐ効果も高い
さらにRustではそこに内部可変性が用意されているため
そのルールを守ったまま複数のデータ更新者(ex.マルチスレッド)が排他制御しながら同じデータを書き換えることも可能
894: 01/25(土)03:45 ID:LC7IJQQw(1) AAS
構ってもらえる相手を探し求めさまよう某
895(1): 01/25(土)10:55 ID:iLzbIZXE(1/3) AAS
>>891 その数論幾何の人にプログラミング言語を作ってもらえばいいんでね
896: 01/25(土)11:31 ID:wB2yLAW7(1) AAS
新商品を作ることにより今後の支障がなくなるといつから錯覚していた
897(1): 01/25(土)15:36 ID:OwaQndIK(1) AAS
>>895
すでに表記の体系はある
CS畑のやつが処理系を作ればいい
898: 01/25(土)17:09 ID:JNkrrIX3(1) AAS
ここまでWolframの話題なし
899: 01/25(土)17:25 ID:W3I6NstP(1) AAS
rustがどうのとかいってるレベルだからね
900(2): 01/25(土)20:44 ID:iLzbIZXE(2/3) AAS
>>897 それはMathematicaじゃダメなん？
表記の体系って、プログラミングするには演算子の優先順位を決めないといけないがそれも決まってるの？
CSやってて数学のわからないところは記号の優先順位がわからなくて読み解けないことがある点
901: 01/25(土)22:15 ID:wEoGbTgh(1) AAS
>>900
だめに決まってるじゃん
902: 01/25(土)22:33 ID:LqupDpHB(1) AAS
>>900
Mathematicaは数式処理システムだ
903(1): 01/25(土)22:57 ID:iLzbIZXE(3/3) AAS
数論幾何用のソフトウェアがないってことかね、表記の体系はどこでみれるの
グレブナー基底とかならRisa/Asirとか群論ならgapとか
多分数学の分野ごとにソフトウェアがあるのが現状だと思う
904: 01/25(土)23:20 ID:T4wakzBv(1) AAS
内容がわからないなら無理に書き込まなくていいのに
905: 01/26(日)01:21 ID:RxnNQ4s+(1/3) AAS
必要なのはドリルではなく穴
記号ではなく意味
と思うじゃん？
906: 01/26(日)07:09 ID:8U3hDZ20(1) AAS
>>903
アホすぎて返す言葉もない
907: 01/26(日)07:29 ID:xKZhC4SH(1) AAS
ID:iLzbIZXE こういう現代文なら零点のレス返してくる人って、日々の生活相当苦労してそうだな
908: 01/26(日)15:13 ID:RxnNQ4s+(2/3) AAS
試験はギリギリ解けないレベルまで難化する
トーナメントは敗者で埋め尽くされる
909: 01/26(日)20:27 ID:m+VDOodg(1) AAS
レベル、経験値、ポイント、HP、通貨、メッセージ数、フレンド数
4（死）、13（キリスト教における忌み数字）
18（嫌）、24（〜に死）、34（〜さん死）
40、42、44
56（殺）、64（無視）
省3
910: 01/26(日)20:55 ID:BcwcPe/+(1) AAS
ドリル優子が大臣に
911: 01/26(日)22:29 ID:RxnNQ4s+(3/3) AAS
経験的なデータはリセットできるからリセット不可能なものと分断されたり見下されたりする
912: 01/26(日)22:57 ID:s+0AyHDZ(1) AAS
ごみはしんでもごみ
913: 01/27(月)08:24 ID:Lwj4/s6G(1) AAS
そう言えばPASCALのスレ無くなってるな
(ObjectPASCALやDelphi除く)
914: 01/28(火)00:55 ID:IzCMkZvk(1/3) AAS
スレタイ、レス件数、スレ作成日、投稿時刻に4や13、忌み数字を使って嫌がらせするネットストーカー、SNSストーカー業者がキモすぎ
4や13などの忌み数字と以下の情報、ポケベル暗号の数字などを（近い位置の並びで）組み合わせて使われていたら嫌がらせの可能性高し。
・名前やニックネーム
・生年月日
・住所、番地
・車のナンバー
・電話番号やメールアドレス
915: 01/28(火)00:57 ID:IzCMkZvk(2/3) AAS
業者の嫌がらせ数字組み合わせ
.204 〜に死
.214 21日生まれ（記念日の人）死
.224 夫婦死
.234 兄さん、爺さん死
.244 西死
.254 事故死、事後死、ニコ死
省15
916: 01/28(火)06:05 ID:IzCMkZvk(3/3) AAS
閲覧171人とか174人、179人、180人、184人
／総視聴者数 （配信者の名前やID、誕生日などの語呂合わせ数字）
数字操作の嫌がらせがキモすぎ
917(1): 01/28(火)10:01 ID:dqvH8r5C(1) AAS
暗号化技術とガロア体の関係を教えて下さい
918: 01/28(火)15:48 ID:fgheZtrX(1) AAS
>>917
暗号化技術でガロアとの肉体関係
919: 01/29(水)21:16 ID:VEYwrfKC(1) AAS
忌み数字を踏ませる業者、アプリ、コンピュータプログラムの嫌がらせ
動画再生回数、表示回数、登録者数、フォロワー数、評価数、コメント数、レベル、経験値、ポイント、HP、通貨、価格、メッセージ数、通知数、フレンド数
4（死）、13（キリスト教における忌み数字）
18（嫌）、24（〜に死）、34（〜さん死）
40、42、44
省4
920: 01/30(木)01:47 ID:pmUo+geg(1) AAS
サブタイピングは本当に必要なのか？
921: 01/30(木)06:49 ID:b37CpeH6(1) AAS
サブタイピングはトポス
922: 01/31(金)21:06 ID:SiR55I1h(1) AAS
閲覧171人とか174人、179人、180人、184人
／総視聴者数 （配信者の名前やID、誕生日などの語呂合わせ数字）
数字操作の嫌がらせがキモすぎ
競合配信者の名前、ポケベル数字、不吉数字の組み合わせ嫌がらせがキモすぎ
忌み数字が表示されやすくなる仕様のクソアプリ、数字操作がキモすぎ
923: 02/01(土)11:40 ID:sUYLXBXm(1) AAS
お薬のもうね
171 いいないい
174 いいな良い
179 いいな休憩
180 飛躍(百) ハッピー 自由(十)
184 飛躍 ハッピー 幸せ
924: 02/02(日)23:57 ID:Drgu6Qh4(1) AAS
口コミや地域マップの表示回数やいいね件数、コメント数、フォロワー数、投稿時刻、通知件数、レビュー評価等で、意図的に忌み数字や悪意のあるポケベル暗号数字をしつこく強調する町内会員の嫌がらせがキモすぎ
例
4（死）、13（キリスト教における忌み数字）
18（嫌）、24（〜に死）、34（〜さん死）
40、42、44
56（殺）、64（無視）
省3
925: 02/03(月)11:27 ID:WyTS2dKB(1) AAS
お薬のもうね
926: 02/03(月)12:07 ID:wBItYUjQ(1) AAS
3が付くときと3の倍数でアホになる
927: 02/03(月)17:58 ID:D+cWD+hu(1/3) AAS
無から有は生じない
928: 02/03(月)17:58 ID:D+cWD+hu(2/3) AAS
型はクライスリ圏の対象
929: 02/03(月)17:59 ID:D+cWD+hu(3/3) AAS
極限は普遍性
普遍性は表現
すべてはカン拡張
930: 02/03(月)19:18 ID:zeOU8J2H(1) AAS
スケッチ→スキャッフォルド→スキーマ
これが数学的プログラミングの骨格
931: 02/03(月)21:26 ID:lZjIFBNe(1) AAS
とりあえずフロントエンドは度外視
あれはJSで動かせるただのオモチャ
932: 02/03(月)23:48 ID:XBLKOMOL(1) AAS
仕様記述言語というのがあってだな
933: 02/04(火)02:03 ID:axINJClc(1) AAS
装飾と結合
934: 02/04(火)03:58 ID:Mw0YRrvx(1) AAS
モナド
再帰と不動点コンビネータ
継続と背理法
935: 02/04(火)12:25 ID:AbihjpY6(1) AAS
BNF
936: 02/04(火)15:34 ID:uhr4OKyS(1) AAS
普遍性は不動点である
937: 02/04(火)20:57 ID:Oeo4Jry5(1) AAS
Wolfram Languageの使い方を聞きに来たんだが
新しくスレ立てた方がよい？
938: 02/04(火)21:27 ID:Es9g2xhz(1) AAS
そうだな
939: 02/04(火)21:28 ID:kCOYqPIc(1) AAS
存在は普遍性
普遍性は極限
極限は不動点
つまり、存在は不動点
940: 02/05(水)02:27 ID:yJbYA8kV(1) AAS
場の臨界点
上下前次1-新書関写板覧索設栞歴
あと 62 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.031s