[過去ﾛｸﾞ] 「数学」をプログラミングするには (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
806: 01/13(月)02:40 ID:XXChvl3U(1) AAS
そして、科学論文の体裁は重要だが、オブジェクト指向はいまや重要ではない
807: 01/13(月)05:24 ID:elRKgauc(1) AAS
型
並行性
最適化
この3つだよ
今求められてんのは
808: 01/13(月)09:04 ID:PzkYuqRH(1) AAS
求めてないよ
809(2): 01/13(月)09:12 ID:J7wtrzSF(1/2) AAS
俺が大学生だった20年前はオブジェクト指向もCSの一部だったが
教授はカプセル化が一番重要だといってた
研究はされてたけど、アスペクト指向は流行らなかったなー
810: 01/13(月)09:12 ID:6+/RYvQh(1) AAS
で、出ｗｗｗｗインターネットあまのじゃく君ｗｗｗｗｗｗｗ
811: 01/13(月)09:13 ID:wtvPYUbh(1) AAS
>>809
君、勉強できなそうだね
812: 01/13(月)09:42 ID:94WYo5Du(1) AAS
>>809
たった三行でここまで頭悪そうな文章書けるのってある意味才能だな
813: 01/13(月)10:20 ID:Ymx2LteG(1/3) AAS
オブジェクト志向の次はデザインパターンだろ
814: 01/13(月)10:42 ID:LSOaiCCa(1) AAS
カプセル化も全否定されてるけど
いまだにアンダースコアの変数はモヤモヤする
815: 01/13(月)10:43 ID:P3ktA6B0(1) AAS
それも宗教
振り子が逆に振れてるだけ
816(1): 01/13(月)11:39 ID:J7wtrzSF(2/2) AAS
デザインパターン20数個のうち10数個ぐらいはただの高階関数でかけるという研究もある
817: 01/13(月)11:55 ID:Ymx2LteG(2/3) AAS
魔法はなかった
818: 01/13(月)13:02 ID:DTY38xVU(1) AAS
>>816
そして残りの10個はただのアンチパターン
819: 01/13(月)17:18 ID:Ymx2LteG(3/3) AAS
岩波講座 ソフトウェア科学 [基礎]1
計算システム入門
著者 所真理雄 著
刊行日 1988/10/06
ソフトウェアの作成は人間的な作業で，信頼性や生産性の点でいまだに手工業の域にある．こうした現状をふまえ，ソフトウェア作成の方法を示すとともに，その理論と知識を整理し，新しい学問体系として提示する
820: 01/14(火)00:54 ID:eoA7bUR4(1) AAS
なぜ高階関数を使わないのか
εδ論法はなぜεの関数を具体的に構成しないのか
こういうのを体系的に整理したら特定の勢力だけが得をして他は損するんじゃないか
だから整理しない
821: 01/14(火)08:02 ID:WvheYWow(1) AAS
Foo = Bar | Baz
822: 01/14(火)08:15 ID:BEZztBwJ(1) AAS
型⊂クロージャ
823: 01/14(火)12:10 ID:ygjj3afU(1) AAS
型なんて特別なものじゃない
0や1はInt型のオブジェクト、IntはType型のオブジェクト
824(2): 01/14(火)12:50 ID:1hGtsoWq(1) AAS
水の呼吸、壱の型
825: 01/14(火)13:27 ID:2ZQOZttA(1) AAS
>>824
咄嗟にアニメの話出せるとか
おまえすげえ最先端行ってるな
才能の塊かよ
826: 01/14(火)13:30 ID:5ok8hMJ2(1) AAS
>>824
それ知ってるわ
煉獄さんの映画のやつだろ
お前マジでおもしれーな
827(1): 01/14(火)13:58 ID:L1ZxvYgu(1) AAS
型が第一級オブジェクトなら、クロージャを使えば状態つきの型を作れるわけか
828(1): 01/14(火)14:18 ID:x8Aql6YT(1) AAS
有理数型や小数型も作れるのか？
829: 01/14(火)14:29 ID:S4iOQtDV(1/2) AAS
>>827
わざわざ型情報を実行時に変化させてどうすんだ
830: 01/14(火)14:29 ID:S4iOQtDV(2/2) AAS
>>828
お前は低レベルすぎ
831: 01/14(火)20:10 ID:6b3bLxyH(1/2) AAS
有理数型はHaskellやMathematicaにもうある
状態付きの型、考えただけで恐ろしい
832: 01/14(火)20:32 ID:A8xCzIhU(1) AAS
そうやって進化していくものよ
833: 01/14(火)21:00 ID:6b3bLxyH(2/2) AAS
状態付きの計算を行う手順を持った型なら純粋だから許せるけど
状態付きの型なんていらないよ
834: 01/14(火)21:07 ID:KUHcAlDi(1) AAS
君に要るかどうかは関係ない
835: 01/15(水)00:39 ID:v8xz0BVe(1/2) AAS
`f1 = Foo 1`なら、f1の型は`Foo 1`
基本的にはこれでいい
`Foo 1`は `{n: Nat} Foo n`のサブタイプ
`f1`を`Bar :: t -> s`に渡せるのは、`Foo 1`に変換する規則が存在するとき
型検査はそれをコンパイラがチェックすればいい
836: 01/15(水)00:39 ID:v8xz0BVe(2/2) AAS
`f1 = Foo 1`なら、`f1`の型は`Foo 1`
基本的にはこれでいい
`Foo 1`は `{n: Nat} Foo n`のサブタイプ
`f1`を`Bar :: t -> s`に渡せるのは、`Foo 1`を`t`に変換する規則が存在するとき
型検査はそれをコンパイラがチェックすればいい
837: 01/15(水)00:45 ID:2eRf9tIs(1) AAS
ユーザー定義関数から値返せないじゃん
838: 01/15(水)00:50 ID:LknHRWOL(1) AAS
型は実体ではなく注釈か
839(2): 01/15(水)01:13 ID:xsuF+zK/(1) AAS
型っつっても所詮は構造体に名前がついただけ
計算の過程や性質に型付けをしたいんだ
「関数fを抜けたタイミングで、ポインタpは必ず指定の条件をみたす場所を指していなければならない」
こういうのを型で保証したいんだ
840: 01/15(水)01:33 ID:Yf+/cXFX(1) AAS
ぬるぽは実行前に排除する
841(1): 01/15(水)06:39 ID:xj5qHVfP(1) AAS
>>839
理解浅すぎ
数学勉強してないでしょ
842: 01/15(水)08:07 ID:ogU0rXVD(1) AAS
>>841
君が数学で研究職に就いているのでなければ、まず間違いなく君よりは理解してるよ
843: 01/15(水)08:10 ID:zm/Y+w4S(1) AAS
>>839
実行時のアサーションで書けることは、型にできる
844: 01/15(水)08:19 ID:Uf2ceum5(1) AAS
二分探索やクイックソートのロジックが正しいことを型で証明できるか
845: 01/15(水)08:32 ID:nE+pEHV1(1) AAS
数学的帰納法で証明できる
（長さ1の配列に対しては自明
長さ1, 2, ..., k-1に対して正しいと仮定して、長さkに対して証明する）
そのような構造はF代数で定式化できる
846: 01/15(水)08:56 ID:3W/U+R8x(1) AAS
アキュームレータを再帰的に更新していくようなのはF代数に抽象化できる
847: 01/15(水)19:07 ID:8y1isLBr(1) AAS
オブジェクト指向はオワコン
848: 01/16(木)02:12 ID:hp6XExKo(1) AAS
抽象データ型、凝集度、関心の分離などの既存の概念だけで簡潔かつ正確に説明できることをわざわざバズワードに言い換えただけのクソ概念
849: 01/16(木)03:23 ID:DBY13IoQ(1/2) AAS
形式論理とかまじで役に立たんからな
850: 01/16(木)08:27 ID:L1OHI3Vu(1) AAS
実は当たり前にやっていること。関数適用はmodus ponensに相当する
851: 01/16(木)18:56 ID:DBY13IoQ(2/2) AAS
でも役に立たないでしょ
少しは文章読めよガイジ
852: 01/16(木)20:35 ID:FAOk1woG(1/2) AAS
型情報からあまり使ったことない関数でも使い方にあたりがつくのは便利だと思うけどお前はそうではないんだな
853: 01/16(木)20:51 ID:Wo2SWLBc(1) AAS
複素数型も四元数型も定義可能だし、GPUに組み込んで高速で並列演算できるようにしてやれば科学界に革命を起こせるな
854: 01/16(木)21:51 ID:zFtBKiS0(1) AAS
処理系がcall/ccをサポートすることは、直観主義論理に背理法を加えることに相当する
855: 01/16(木)22:19 ID:FAOk1woG(2/2) AAS
研究者の名前がなかなか思い出せなかったがGriffinだな POPL 1990
856: 01/16(木)22:28 ID:l7++KB1R(1) AAS
イマドキ型のない言語なんて、即席のスクリプトくらいにしか使わんでしょ
857(1): 01/16(木)22:31 ID:IceLMl7e(1/2) AAS
代数的データ型やパラメータ多相を使えばプログラムのかなり多くの性質をコンパイラが保証できるのに、わざわざ型検査なしで注意してコード書くとか馬鹿のすること
858: 01/16(木)22:36 ID:IceLMl7e(2/2) AAS
人類未曾有のソフトウェアを書くならともかく、巷のプログラムの9割近くのコードはただデータを整形してマッピングしてるだけ
あとの一割は既存のライブラリの呼び出し
現代のプログラミング言語の型システムがあれば、IDEの入力補完に従ってるだけでバグの無いコードが書ける
画面にらみつけてロジック確認なんかしてんのはただのアホ
859: 01/16(木)22:51 ID:fgdrajER(1) AAS
しかし、それができるなら動的型付けの言語でもエディタが構文から型推論すれば同じことができるのでは？
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の型はトレイト属性があって
マルチスレッドでも同期が保証される型など
抽象度の高い表現が型システムで扱えるようになってるね
それによりデータ競合が起きないことを型システムで保証してしまってるところが凄いと思った
上下前次1-新書関写板覧索設栞歴
あと 116 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.020s