集合論に基づいた言語を作りたいat TECH
集合論に基づいた言語を作りたい - 暇つぶし2ch439:デフォルトの名無しさん
14/10/06 12:01:11.94 DaOiROEZ.net
選択公理って、よーするに、どんな集合からでも「その要素を一つ選んで取り出す」ことができる、
とする公理でしょ。コンピュータでそれを原理として使えない理由ってある?

(本物の実数の濃度を持った集合を表現できない、とか?)

440:デフォルトの名無しさん
14/10/06 12:36:12.97 Fl7PIp2q.net
「無限集合の無限集合」をどう扱うよ?

441:デフォルトの名無しさん
14/10/06 12:55:54.86 DaOiROEZ.net
(ポインタで表される)一つの要素であることに変わりは無いと思うけど

442:デフォルトの名無しさん
14/10/06 13:25:58.86 Fl7PIp2q.net
…解らないなら解らないと正直に言えばいいのに…

443:デフォルトの名無しさん
14/10/06 15:33:29.23 DaOiROEZ.net
説明できないなら(以下略

444:デフォルトの名無しさん
14/10/06 15:44:15.26 Chlrt5UY.net
選択公理は選択する方法があるとは主張するけど、選択する方法を具体的に出す訳じゃないから無問題

445:デフォルトの名無しさん
14/10/06 22:35:03.81 NlMQaHfx.net
>439
可能無限なら扱える。実無限は無理。

>441
自然数で番号付けできているから、実数は扱えない。

>444
実数は選択できないよ。

446:デフォルトの名無しさん
14/10/06 22:39:52.81 DaOiROEZ.net
哲学屋が語る論理の本で勉強したなw

447:1
14/10/06 23:54:52.31 FKIcXs6f.net
なんか計算不能な問題に取り組ませたい奴がいるっぽいな。
>>48と同じ奴か?

448:デフォルトの名無しさん
14/10/07 00:54:44.71 EYnjWx9Z.net
スレタイに釣られるとそうなるよ

449:デフォルトの名無しさん
14/10/07 05:00:08.90 p/BL+CDX.net
DaOiROEZの半可通っぷりが最高w

450:デフォルトの名無しさん
14/10/07 10:56:48.49 +SCn7tHo.net
ZFの範疇でさえ消化できてないのに、実無限なんて飛躍しすぎ。

451:デフォルトの名無しさん
14/10/07 11:06:53.72 SMQvkaFY.net
どうせなら、量子コンピューターで使う言語にまでにして欲しいな。

452:1
14/10/07 21:14:56.86 QnZoLRl/.net
量子コンピュータってまだ有効なアルゴリズムが2つ3つしか発見されてないんじゃなかったけ。

453:デフォルトの名無しさん
14/10/07 21:30:05.48 waP9/Nh6.net
量子状態を集合的に扱うと便利。

454:デフォルトの名無しさん
14/10/07 21:41:15.48 9NXt3xp/.net
>450
少ない公理だけでやるんだったらProlog (HornCNF) で十分だと思う。
というかPrologがろくに検討されていないのはなぜ?

455:1
14/10/07 22:20:49.79 QnZoLRl/.net
Prologもやってみる価値あり?

456:デフォルトの名無しさん
14/10/08 04:21:45.13 prFbm0Ro.net
公理論ベースのプログラミング言語というのにPrologを検討してないとか意味わからなすぎ

457:デフォルトの名無しさん
14/10/08 11:09:43.78 OludtdBn.net
単なる述語論理じゃないか。

458:デフォルトの名無しさん
14/10/08 12:20:34.72 dWGNDTcI.net
>>1ってそもそも集合論、公理的集合論を系統的に学んだこと無いだろ?

459:デフォルトの名無しさん
14/10/08 12:47:37.54 h0nYZNts.net
既存の言語に有限集合演算を追加するところから始めれ。
クソスレが一個増えただけで終わる前に。

460:デフォルトの名無しさん
14/10/08 18:43:36.24 UKHmkXIf.net
ここは元々>>1の勉強スレ

461:1
14/10/08 18:47:59.90 hP0aEtf7.net
>>458
ばれたか。ZFCとか名前くらいは聞いたことあるけど
どうやって論理を展開していくのとか知らない。

>>459
出来ればもうちょっと面白いアイディアが欲しい。
クソスレも板の賑わいってことで。

462:デフォルトの名無しさん
14/10/08 20:19:42.08 rTFjlrrq.net
1が今まで読んできた教科書教えて

463:1
14/10/08 20:46:16.58 hP0aEtf7.net
あんまりいうと個人情報とか洩れるかもしれんので一つだけ。
もう捨てちまって手元にないがこれかな。
URLリンク(www.amazon.co.jp)

464:デフォルトの名無しさん
14/10/08 22:26:27.29 rTFjlrrq.net
じゃあ個人情報が漏れない程度の大雑把さで何を学んできたか教えて

465:1
14/10/08 22:32:55.73 hP0aEtf7.net
そんな漠然としたこと聞かれても。
まあ、情報系の学部出身だよ。

466:デフォルトの名無しさん
14/10/08 23:00:13.01 TzLBQJ9w.net
人生……かな

467:デフォルトの名無しさん
14/10/08 23:04:08.42 rTFjlrrq.net
>>59を見てどの程度の知識があるのか気になったのよ
数学科ではないのね

468:1
14/10/08 23:24:26.28 hP0aEtf7.net
数学科ではないな。
まあ、俺は数学ガチ勢ではないってことで。

469:デフォルトの名無しさん
14/10/08 23:51:56.29 TxL/GihU.net
>>465
それにしてはレベルが低いな。

470:デフォルトの名無しさん
14/10/09 14:59:21.86 +VtBJxY5.net
>スクリプト言語でありながら、速度も求めた Julia という言語。
> Julia は科学技術計算向けだが、汎用的な用途にも使える。
URLリンク(julialang.org)

集合論とはちょっと違うが、こういう言語を作るのって、プログラミングとはまた別の頭の良さが必要なんだろうなあ・・・

471:デフォルトの名無しさん
14/10/09 18:53:47.65 0qGZB94E.net
>>463
こんなの学部一、二年だろ?
URLリンク(www.amazon.co.jp)
こういうの読みなよ。

472:デフォルトの名無しさん
14/10/09 19:18:35.22 tOThY/oR.net
constraint logic programming‥

メジャーなもののなかで一番近い言語はなんですか

473:デフォルトの名無しさん
14/10/09 19:25:16.95 0qGZB94E.net
これのOzだよ。
URLリンク(www.amazon.co.jp)

474:1
14/10/09 20:10:14.35 o/OZDU1F.net
>>469
こんなもんじゃね?

>>470
インタプリタでCに迫る速度とかホンマかいな?
まあ、速くて書きやすいのはいいことだ。

>>471
わざと難しそうなの持ってきてない?

475:デフォルトの名無しさん
14/10/11 12:51:05.92 8yVA6sZ1.net
この板でハッとさせられるような事言う奴滅多にいないんだよな。
たまに居ると思ったら5年前の自分の書き込みだったw

476:デフォルトの名無しさん
14/10/11 13:27:28.71 77jPKn4U.net
>>475
つまり、おまえは5年間進歩してないんだな。

477:デフォルトの名無しさん
14/10/11 15:22:20.55 zm2pT6ST.net
とっくに出てると思うけど、SQLがまさに集合論をベースとしてる
今ではC#がLINQという名前で取り込んでるな

478:デフォルトの名無しさん
14/10/11 16:17:13.48 dB8AJmwd.net
それは集合論ではない。
集合や集合演算を扱えるだけ。

479:デフォルトの名無しさん
14/10/11 17:10:54.15 LAagPdIX.net
>>477
それSQLじゃなくてRDBシステムが集合論つかってるってことじゃないのか?

480:デフォルトの名無しさん
14/10/11 18:08:16.60 F3plGA7W.net
集合操作だから集合論とか言うの止めてくれないか

481:デフォルトの名無しさん
14/10/11 20:16:24.89 77jPKn4U.net
SQLは集合論つーより代数論だ。

482:デフォルトの名無しさん
14/10/11 20:16:36.33 oD37Hh5X.net
別に素朴集合論に単純な型を付けたようなもので普通に用は足りるだろ。
公理的集合論だからといって現実的には何かできることが増えるわけじゃないぞ。
単に数学の基礎を議論する時に必要というだけで。

483:デフォルトの名無しさん
14/10/11 20:18:28.72 77jPKn4U.net
>>482
その程度のものなら既存で腐る程あるだろ、って話を何度ループすれば気が済むんだ?

484:デフォルトの名無しさん
14/10/11 22:48:51.28 oD37Hh5X.net
で、集合論に何を夢見てるんだ?

485:デフォルトの名無しさん
14/10/12 00:31:12.35 xA+0V9C8.net
素朴集合論ってカントールの集合論のことだぞ。
中学生が習うやつじゃないぞ。

486:デフォルトの名無しさん
14/10/12 02:13:46.33 UDZcvZvs.net
カントンが手術したらモテモテになると勘違いしている様>>1

487:デフォルトの名無しさん
14/10/12 20:49:20.54 MyToBo/B.net
だから「単純な型を付けたようなもの」って言ってるだろ。
その意味がわかってない?

488:デフォルトの名無しさん
14/10/12 20:55:04.62 g8Gog7KJ.net
お前が分かってない。

489:デフォルトの名無しさん
14/10/12 21:08:23.19 Sn9uUxXA.net
なんとなくだけど、結論を急いで、できないとか意味がないとか言って、一切の建設的な意見を出さず、妨害だけする人って居るよね?

490:デフォルトの名無しさん
14/10/12 21:17:15.44 g1iKtf1h.net
そりゃこの広い世界のどこかにはそういう人も居るかもしれないね

491:デフォルトの名無しさん
14/10/12 21:35:02.06 xA+0V9C8.net
素朴集合論に型を付けたらうまくいくんじゃね?
とやってみたら恐ろしく複雑で不自由になったのがフレーゲのタイプ理論。
その後100年近く塩漬け状態。
それなら集合とクラスの二つだけに分けて、後はあまり強く型付けしなければ、
カントールの楽園から追放されないんじゃね?
というのがツェルメロの公理的集合論。

集合論、集合論と言っている人は、
無限公理や正則性公理を積極的に言語で使うつもりがあるのかな?
↓必要なのはここまでなんじゃないのかな。
URLリンク(ja.wikipedia.org)

492:デフォルトの名無しさん
14/10/12 22:31:37.21 NJmCyxXF.net
>>489
どのレス?

493:デフォルトの名無しさん
14/10/12 22:35:38.76 A+IMFSgX.net
S Set
T Theory
P Programming

Aはどうしよう。

494:デフォルトの名無しさん
14/10/12 22:38:10.76 Km5KyqRm.net
advanced
application
applied

495:デフォルトの名無しさん
14/10/12 22:44:43.09 Km5KyqRm.net
the set theory applied programming (STAP) language

略してSTAP言語

496:デフォルトの名無しさん
14/10/13 00:27:06.12 ivWOljm1.net
で、できたの?

497:デフォルトの名無しさん
14/10/13 00:34:39.55 hWTf/9FL.net
200回ぐらい。

498:デフォルトの名無しさん
14/10/13 05:17:51.25 zgXTsI5w.net
>>489
既存研究のサーベイが皆無なバカが悪い

499:デフォルトの名無しさん
14/10/13 09:30:42.66 7i+sJhXA.net
>>496
ありま~す

500:デフォルトの名無しさん
14/10/13 17:01:25.51 6ak88RQb.net
1.動機
2.仕様
3.実装
と進む。前段階へのフィードバックもある。
まだ1.の整理がつけられてない状況。

501:デフォルトの名無しさん
14/10/13 18:07:14.67 UPM0IlOC.net
まずどんな出力を得たいかを書く
次にそれを得るのに入力に何が必要かを書く
これで仕様決めまで終わるよね
入出力が決まってれば実装手段なんて何でもいい

502:デフォルトの名無しさん
14/10/13 19:11:43.08 PQyRtfoA.net
こういう状態
>>425 >>428

503:デフォルトの名無しさん
14/10/13 20:12:54.48 EYFsbw6u.net
オブジェクトは全て集合で
ペアノの公理を入力したらそれに則って足し算ができるようになる言語は
どうかな?

504:デフォルトの名無しさん
14/10/13 20:22:39.44 5XmBCMSV.net
足し算しかないのはプレスバーガー算術といって、完全理論だよ
(どの命題も肯定か否定かどちらか一方が証明可能って意味)
足し算とかけ算の混じったペアノ算術は不完全理論だけど

505:デフォルトの名無しさん
14/10/13 22:25:59.32 6ak88RQb.net
>>503
ノイマンの自然数の構成も必要だぞ。

506:デフォルトの名無しさん
14/10/14 09:11:24.51 0Ml7fYIK.net
集合への四則演算は濃度に変化無しだよな?
即ち、四則演算はしなくていいって事。

507:デフォルトの名無しさん
14/10/14 13:04:54.64 vbP2sDzC.net
濃度を増やすことが目的じゃなくて
計算結果を求めるのが目的だろうが

508:デフォルトの名無しさん
14/10/14 14:33:07.44 zPTDiwn8.net
これとかいいんじゃね
スレリンク(tech板)

509:デフォルトの名無しさん
14/10/14 17:47:21.71 +5iJxgCE.net
外野として面白く見守ってるだけでいうのもアレだけど
具体的に章末問題をひとつ持ってきて「これをこう書きたい」っていうのがみたい!
1さんだけじゃなくてここに居る皆さんで「こう書いたら気持ちよさそう~」とかでいいからサ

510:デフォルトの名無しさん
14/10/14 19:09:39.61 bR6+1Vd4.net
0=φ
1={φ}
2={φ{φ}}
3={φ{φ}{φ{φ}}}
4={φ{φ}{φ{φ}}{φ{φ}{φ{φ}}}}

は良いとして、このノイマンの表現法で通常の4則演算ってどういう意味があるの?
2+2=4  ってこの右側の集合の記法でどうやってでてくるんだ??

511:デフォルトの名無しさん
14/10/14 20:03:06.07 ehQP27NF.net
ラムダ ペアノ でググれ

512:デフォルトの名無しさん
14/10/14 20:40:10.02 bR6+1Vd4.net
>>511
ラムダとペアノの奴っていうのは

後者関数と射影関数を使って原始帰納法から原始帰納的関数を定義する方法で
加算を定義するというものと内容的に同値だろうから、

この自然数を包含関係で表現してみた集合に対する演算の定義とは違わないか?

513:デフォルトの名無しさん
14/10/15 07:50:36.68 xIPL4/1H.net
>>510
それはまず
0:=φ
succ(x):=x∪{x}
があって、そこから
1:=succ(0)=φ∪{φ}={φ}
2:=succ(1)={φ}∪{{φ}}={φ∪{φ}}

と順に定義していくから
結局はペアノの焼き直しに過ぎない

514:デフォルトの名無しさん
14/10/16 00:40:06.63 txhx6QUq.net
>>510
四則演算の意味は四則演算w

ペアノの公理に出てくるプリミティブを定義しないといけないから、
succは>>513、lessは∈に帰着させる。
たぶんlessを先に考えたのだろう。

515:デフォルトの名無しさん
14/10/17 13:53:23.37 dWEICMsc.net
>>511
ノイマンの集合モデルとチャーチのラムダ式モデル(チャーチ数)は、ペアノの自然数の別のモデル。

516:1
14/10/17 22:20:25.82 XLlp2k/U.net
最近書き込むネタがないな。
>>509
なんかお題くれ。

517:デフォルトの名無しさん
14/10/17 22:55:41.78 ZbpwpO5Z.net
>>516
一つの海によって隔てられた2つの国の領土が与えられたときに、海上に2国の中間線を引くプログラムを作れ
ここで、中間線とは2国の海岸線から等距離になるような線のことである

518:1
14/10/17 23:03:16.81 XLlp2k/U.net
まためんどくさそうな問題を。。。
海岸線のデータは多角形で与えられるの?
入力データ作るだけもでかなり面倒だなぁ。

519:1
14/10/17 23:20:00.94 XLlp2k/U.net
できれば100ステップくらいで実装できるの希望。

520:1
14/10/17 23:30:05.44 XLlp2k/U.net
垂直二等分線がカギになるのかな。
どっちにしろむずかしすぎ。

521:デフォルトの名無しさん
14/10/17 23:53:33.32 Dp+Vl0QI.net
関数型言語(笑)でいいと思うよ

522:デフォルトの名無しさん
14/10/18 00:33:49.53 8XT1TYTP.net
>>516
どの教科書に載っているどういう問題をどのように書ける言語にしたいのか、1が言わなきゃどうしようもない。
>>62 >>75 >>83 >>300 >>305

523:1
14/10/18 09:56:05.69 JlR7w5XX.net
>>522
教科書は離散数学とかアルゴリズムのやつで。
どのように書ける言語にしたいかはまだアイディアないってことで。
みんなで雑談するうちになんか出てくればいいなと思ってる。

524:デフォルトの名無しさん
14/10/18 12:22:35.42 /oNwCDSd.net
>>517
実際のデータをおいている場所をご存知のかたはおられませんか?

525:デフォルトの名無しさん
14/10/18 14:38:07.57 8EPYxHvD.net
>>523
(まだ手元にある>>463)教科書や扱いたい問題を「いくつか具体的に」示せ、
言語仕様も叩き台になるものを示せ、
1がそうしたことすらやらないんじゃどうしようもない、
ってことだろうに。

URLリンク(www.weblio.jp)

526:デフォルトの名無しさん
14/10/18 14:48:23.34 MO+ZAloR.net
SymPyでいいよ。
URLリンク(docs.sympy.org)

527:1
14/10/18 19:42:31.60 JlR7w5XX.net
>>524
データ出されてもこんな問題多分とけんぞ。
仮に解けたとしても相当時間かかる。

>>525
もう俺はネタもってない。

>>526
無限あつかうのか。よくこれでまともに動くな。驚くわ。

528:デフォルトの名無しさん
14/10/18 21:20:22.32 zBDuzTiF.net
>>527
自分の持ってる本に載ってる問題の中から一つ挙げてくれるだけでもいいと思うよ
あと、他人の協力を必要としてるのに他人の出した問題にケチをつけるのはよくないよ

529:1
14/10/18 21:42:25.30 JlR7w5XX.net
>>528
ケチつけるというか、難易度が半端ないんだが。
もうちょっとお手軽に楽しめるお題を期待していた。

それと本からじゃないけど暇つぶしに一個出題。

一本の紐がありこれを次の操作を9回繰り返して切断する。

操作「今ある紐の断片からランダムに一つ選択し三等分する。」

この操作を行った後、紐の断片をランダムに2つ選択する。
2つの断片の長さが等しい確率を求めよ。

※未解決な問題
操作をn回行った後断片をランダムに2つ選択したとき長さが等しい確率をp(n)とおく。
lim[n→∞]p(n)はいくつになるか。

530:デフォルトの名無しさん
14/10/18 22:05:05.10 nO1Wa2kk.net
これに計算機必要なの?

531:1
14/10/18 22:12:35.28 JlR7w5XX.net
>>530
手計算でやりたいなら止めないが。

532:デフォルトの名無しさん
14/10/18 23:08:22.47 e6RQ0dr6.net
継続中
>>425 >>428

今度はプログラミング言語と関係ない問題をだしてみたり

533:1
14/10/18 23:22:35.69 JlR7w5XX.net
>>532
まあ、ネタもないしな。
このスレは基本雑談ってことで。

534:デフォルトの名無しさん
14/10/19 09:37:05.49 29Wx6lEI.net
あらら。
集合論関係無く、集合操作したかったってことでしょ?
で、聞いてみたら既にいろんな言語(ライブラリ)が存在したと。

535:1
14/10/19 17:36:40.59 juftpz1M.net
>>534
まあ少し面白い話にならないかと期待してた。
具体的なアイディアはないんだが。

536:デフォルトの名無しさん
14/10/19 17:46:26.61 SfAoaW7H.net
>>535
まだ手元にある離散数学やアルゴリズムの教科書や、それに載ってる演習問題を挙げる
程度のことすらしないのはなぜ? その程度で

>>463
個人情報とか洩れる

わけがないのに。

537:1
14/10/19 19:25:17.13 juftpz1M.net
>>535
×まあ少し
○もう少し

>>536
じゃあ、まあ、教科書から一個出題。

ニ?ゲームはスティックの山の集まりを用いたゲームである。
一つの手番でプレーヤーはどれか一つの山から1個以上のスティックを取ることができる。
プレーヤーは交互に順番に手番を行う。そして最後のスティックを取るプレーヤーを負けとする。
いま、ニ?ゲームの局面としてs_1,s_2,...,s_k本のスティックからなるk個の山が与えられているとする。
与えられた局面に対し、先手必勝かどうかを判定せよ。

538:1
14/10/19 19:29:53.16 juftpz1M.net
あれ、文字化けしてんなぁ。
ニムゲームね。

539:1
14/10/19 21:14:49.94 juftpz1M.net
ちなみに>>529の問題はRubyで689byteで実装できた。
もっと短くかける言語があるよ!という人がいたら教えて。

540:デフォルトの名無しさん
14/10/19 21:24:53.85 CFixaMQx.net
>>537
まだ手元にある離散数学やアルゴリズムの教科書を何冊か挙げる程度のことすらしないのはなぜ?

541:1
14/10/19 21:38:28.27 juftpz1M.net
>>540
これとか。
URLリンク(www.amazon.co.jp)
もう捨てちまってあんまり持ってないんだよ。

542:デフォルトの名無しさん
14/10/19 22:07:12.36 C9CvfGxs.net
教科書捨てる奴ってw 学術的な研究はとっとと諦めた方がいい。向いてない。

543:デフォルトの名無しさん
14/10/19 22:15:08.20 lrejmkiS.net
>>541
「あんまり」じゃなくて「一冊しか」だろ。

544:1
14/10/19 22:20:34.02 juftpz1M.net
>>542
まあな。

>>543
そう責めるな。

545:デフォルトの名無しさん
14/10/19 22:28:38.99 N1Fbmuag.net
>>541
捨てたんじゃなくて元からその一冊しか持ってなかったんだろ。
で、その本を読んで「集合ってスゲー」と思い、勢いでこのスレを立ててしまったと。

546:1
14/10/19 22:38:57.73 juftpz1M.net
>>545
学生のころ使ってた教科書はほとんど捨てたよ。
まあ、勢いでスレたてたのは認める。

547:デフォルトの名無しさん
14/10/20 09:04:25.01 jBlrymD4.net
>>533
> このスレは基本雑談ってことで。
君は軽い気持ちで立てたスレかもしれないが、多くの住民はム板にクソスレを立てるべきではないと感じている。
だから君への風当たりが強いのである。
雑談なら雑談スレやブログやVIPでやればよい。まあ、このスレを使い切った後にな。

548:デフォルトの名無しさん
14/10/20 10:17:53.34 UiYQrarC.net
だから、巡回セールスマン問題とかの為に、量子コンピューター用の言語にすればいいのに。

549:デフォルトの名無しさん
14/10/20 12:52:46.72 C1FZ+AtI.net
とりあえず圏論を学習してからにしてくれ

550:デフォルトの名無しさん
14/10/20 18:45:10.40 9HS8Ctp3.net
>>546
で、結局何がしたいの?後出しジャンケンがしたかっただけ?

551:1
14/10/20 19:25:51.34 TfUqLiTt.net
>>547
まじで。

>>548
量子コンピュータでNP完全問題って多項式時間でとけるようになったのか。
時代は進歩してるな。

>>549
じゃあ、>>549が教えてくれ。

>>550
後出しジャンケンといわれても困るんだが。

552:デフォルトの名無しさん
14/10/20 20:21:35.78 4bxYYw/L.net
教科書捨てるくらいだから頭の中空なんだろ。アイディアもない。
普通ならアホなアイティアで収拾つかなくなってなきゃいけない。
そういうカオスが偶然ぷよぷよみたいに連鎖して新しい発想になる。
才能無い人が努力やコミュ力で才能ある人を打ち負かすっていう
根性論はもう見飽きた。

553:1
14/10/20 20:43:37.79 TfUqLiTt.net
>才能無い人が努力やコミュ力で才能ある人を打ち負かすっていう
アニメかなんかか?

554:デフォルトの名無しさん
14/10/20 20:58:59.44 4bxYYw/L.net
デスマーチとかやってるのは才能ないやつ(納期ギリギリまで上流工程やってる上司+素人同然のコーダー)を寄せ集めてやってるからだと思う。
だから デスマーチ=根性論 と思っている。断っておくが、アニメの話でもある。

555:1
14/10/20 22:04:32.06 TfUqLiTt.net
なぜに突然デスマーチ?
カオスだ偶然だで新しい発想は出ないと思うぞ。
根性からはでるかもしれんが。
まあ、新しいものってのはセオリーに裏打ちされてるもんだよ大抵。

556:デフォルトの名無しさん
14/10/20 22:15:50.47 4bxYYw/L.net
ある世界Aには学術体系、理論体系が構築されている。
もう一つの世界Bがゴチャゴチャのカオスだとする。
AとBの間には写像のように紐付けがされている。
発想は世界Bから生まれる。
世界Bが空なのが1だ。

557:1
14/10/20 23:08:08.26 TfUqLiTt.net
>>556
まじでそんな世界観で生きてんの?
アニメの見すぎじゃね?

558:デフォルトの名無しさん
14/10/20 23:17:33.77 4bxYYw/L.net
世界Bが空というのは「頭が空」という意味だから言い過ぎた。すまん。
>>1の発想が尽きたのは、
世界Aの一部と世界Bが一対一対応で同じだからか、
世界Bがあまりに小さいからだと考えられる。

559:デフォルトの名無しさん
14/10/21 04:55:39.53 55M9GoPd.net
>>551
クレクレ言うから条件に合いそうなものを提供すると、
別の条件を出してソレジャナイと言う。
かといって、自分から何かを提供するわけでもない。
ひたすらクレクレ言い続けて、ソレジャナイと返し続ける。

そういうのを後出しジャンケンと言う。

560:デフォルトの名無しさん
14/10/21 05:07:05.92 rC2hZRaT.net
後出しかぁ
どうせなら中出しの方がいいな

561:デフォルトの名無しさん
14/10/21 08:21:27.32 7wZlZLdP.net
ジャンケンドピュッ

562:デフォルトの名無しさん
14/10/21 11:02:34.86 yoqXS5RA.net
このチラ裏まだやってたのか
まだ見限ってない人がいるんだな

563:デフォルトの名無しさん
14/10/21 14:21:29.74 3SFXCOz9.net
>>559
本当にそれのくりかえしだもんな。

564:1
14/10/21 19:14:06.10 +255aWxA.net
>>559
>>563
今の状態で後出しジャンケンというなら、今後も後出しジャンケンは続くとしか言えないな。
まあ、愛想をつかすというなら>>559>>563の勝手だよ。

565:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/10/21 20:10:33.19 tyo0JEbH.net
>>1
ネタ切れか? まずは、命題論理を実装した言語を作ってもらいたい。

a = true;
b = false;
c = a && b;
println c; //false

さあ、できるかな?

566:デフォルトの名無しさん
14/10/21 20:13:11.64 rAN/sZsH.net
後出しジャンケン継続宣言w

567:1
14/10/21 20:34:57.34 +255aWxA.net
>>565
C++でいいんじゃないか。

>>566
まあ、俺の技量には限界があるからな。

568:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/10/21 20:46:47.47 tyo0JEbH.net
>>1は、大学か独学でコンパイラやスクリプト言語の作り方の勉強をしたのかね?

569:1
14/10/21 21:00:41.61 +255aWxA.net
>>568
さわりだけ。
ぶっちゃけ、ひらがな電卓はかなりすごいと思う。

570:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/10/21 21:08:49.12 tyo0JEbH.net
新しく言語を作るなら、バックエンドはGCC系、LLVM系、他言語変換系(Java,JS,C,C++)のいずれかが妥当だろうな。

571:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/10/21 21:21:00.17 tyo0JEbH.net
GCCで作るなら、GDCのソースを読むべし。

GDC (D Programming Language for GCC)

572:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/10/21 21:27:37.89 tyo0JEbH.net
言語変換で作るなら、Pascal⇔C変換プログラムのソースを読むべし。

573:1
14/10/21 21:28:12.21 +255aWxA.net
LLVMとか多分無理。
他言語変換系がいいかな。
個人的にはRubyが好みなんだが。

574:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/10/21 21:57:41.40 tyo0JEbH.net
Ruby上で推論・数式処理・計算をする実行時モジュール作ればいいんじゃね?

575:1
14/10/21 22:36:26.49 +255aWxA.net
なぜに突然、推論、数式処理がでてくるのかわからんが。
わざと面倒くさそうなの持ってきてない?

576:デフォルトの名無しさん
14/10/22 05:45:57.21 wja3nREO.net
集合論扱うのに必須だからだろ

577:デフォルトの名無しさん
14/10/22 05:48:31.37 wja3nREO.net
ルビ厨ってこんなんばっかり
威勢のいいこと言うだけで自分は何もしない
他人や他言語の成果に乗っかるだけ

578:デフォルトの名無しさん
14/10/22 15:09:01.24 WTBQKchq.net
Rubyまでとばっちりw

579:デフォルトの名無しさん
14/10/22 18:30:22.20 kKncjr9Q.net
>>559
「わざと難しそうなの持ってきてない? 」「わざと面倒くさそうなの持ってきてない?」と言ってみたり >>474 >>575

580:デフォルトの名無しさん
14/10/22 19:56:19.33 fCfdG1e1.net
>>517
二つの海岸線を曲線L1, L2とおいた時に、あるp(x,y)∈L1と曲線L2との中間点を
pとpを通る傾き-dx/dyの直線lとL2との交点との間にひかれる線分の中点とすると、
二つの海岸線の中間線はこの中点を集めたものになる?

581:デフォルトの名無しさん
14/10/22 22:36:02.17 iNJY0L1E.net
設問の矛盾が問題ややこしくしているだけ。
その矛盾とは湾だ。湾を除外すれば簡単になる←このへんの要領の良さが仕事では重要。
まず陸地に外接する凹みのない多角形を生成すればいい。
次に各国の外接多角形どうしから等距離の点の軌道を求めればよい。

582:デフォルトの名無しさん
14/10/22 22:41:47.09 iNJY0L1E.net
国Aの外接多角形上の点を定めれば、そこから国Bへの最短距離の線分が定まる。その中間点は明らかに
国Bから同様の手順で求めた中間点と同じだ。だからその軌道で中間線は定まる。

583:デフォルトの名無しさん
14/10/22 22:49:57.00 iNJY0L1E.net
なお凸な外接多角形を用いない場合、中間線は定まらない。

584:デフォルトの名無しさん
14/10/22 23:34:03.55 iNJY0L1E.net
設問(仕事における設計)を改変したことで怒られることはありえるので、アホ設計者に相談するのが先決である。

585:デフォルトの名無しさん
14/10/22 23:58:12.26 iNJY0L1E.net
定まらなくもないか、凹の部分の曲率が、相手国から引いた最短距離を半径とする円より小さいならば定まる。

586:デフォルトの名無しさん
14/10/23 01:20:06.15 mtwqOq23.net
ああそっか、最短距離でいいのか…いらんこと考えて複雑にしてたthx
URLリンク(pastebin.com)

587:デフォルトの名無しさん
14/10/23 01:51:05.76 B12M++5h.net
何がムカつくって、>1が何もするつもりが無さそうなのに成果だけクレクレ言っているところだよな。

>1はPrologについて調査したのか?

588:デフォルトの名無しさん
14/10/23 02:14:57.76 TE8bWo7Y.net
最短距離じゃない。線分とそれを微小移動させた線分とが作る平行四辺形の密度が全海域に渡って一定となるように微小移動(速度関数)を決めればいいのか。
微分積分の問題。

589:デフォルトの名無しさん
14/10/23 02:16:30.21 TE8bWo7Y.net
平行四辺形じゃなくて四角形 ,ねじれて2つの三角形になることもある。

590:デフォルトの名無しさん
14/10/23 02:20:07.97 TE8bWo7Y.net
ねじれて2つの三角形になることもある→ない。

591:デフォルトの名無しさん
14/10/23 04:45:24.37 xJ2edcK8.net
で、それのどこが集合論?

592:デフォルトの名無しさん
14/10/23 04:46:42.26 dXJn7cDs.net
ID:TE8bWo7Y は病気なんです。何も言わずにNGして下さい

593:デフォルトの名無しさん
14/10/23 09:00:17.01 xLBbOXbP.net
>>588
別に海岸線上の点を連続的に動かす必要ないでしょ
一般に距離空間において点Pから集合A,Bまでの距離をそれぞれd(P,A),d(P,B)とおくと
これらは連続関数になるからd(P,A)=d(P,B)を満たす点Pの集合を求めりゃいいだけ

594:デフォルトの名無しさん
14/10/23 12:20:33.04 TE8bWo7Y.net
海岸線を微分するためには連続関数にしなければならない。
そのためにはまずB-spline曲線近似する必要がある。
プロットした点を除外し再計算することでB-splineから湾を除去することもできる。
このように海岸線をパラメトリック曲線で表すことにより
パラメータの範囲を求めることができる。
どのように求めるかというと2つのパラメトリック曲線上の点が
2つの海岸線の共通の接線となる値を求め、それの最大と最小を求めればいいのだ。
これにより分割すべき海域が求まる。
次に海域を等密度で並ぶ線を求めることを考える。

595:デフォルトの名無しさん
14/10/23 12:25:21.29 TE8bWo7Y.net
訂正;2つのパラメトリック曲線上の点が→2つのパラメトリック曲線上の点を通る線が

596:デフォルトの名無しさん
14/10/23 12:40:29.47 TE8bWo7Y.net
そんなことしなくてもいいか。
2つのB-spline曲線上の点を結ぶ線分で、他の箇所と交わらないようにパラメータの最大と最小を求めればいい。

597:1
14/10/23 18:46:19.11 gc7yGcGD.net
>>587
Prologだとどんな問題がHaskell,Rubyよりうまく解けるの?
なるべく人為的でない自然な問題希望。

>>596
すげぇ難しそうですね。
俺はもうギブアップです。

598:デフォルトの名無しさん
14/10/23 19:35:25.06 xJ2edcK8.net
B-spline以外にもC1連続な曲線なんていくらでもあるだろ

599:デフォルトの名無しさん
14/10/23 19:39:22.10 TE8bWo7Y.net
さて2つのB-spline曲線をF(t),G(t) とする。
2つの曲線上の点を結ぶ大陸間横断線分が海域を等密度で並ぶようにし,F,G間の関係式を求めてみよう。
まずその線分が微小移動したときにできる細い四角形の面積を求める。
2つのベクトルのなす三角形の面積の外積公式より
A=(1/2)*|ΔF×L|
B=(1/2)*|ΔG×(-L)| (面積が負にならないようにベクトルの向きを逆にするといい)
A+Bが細い四角形の面積であり、これを大陸間横断線分の長さ|L|で割ったものを密度と定義し一定であればよい。
なおLは大陸間横断線分のベクトルであり、後に積分するので移動前と移動後とは近似できる。
(A+B)/|L|=C ただしCは定数
A+B=C*|L|と変形し両辺積分する。積分範囲は上記ですでに求めてある。
∫Adt+∫Bdt=曲線の長さの関数の定数倍=c(t)
F(t)=F(Fx(t),Fy(t)),G(t)=G(Gx(t),Gy(t))とすると
c(t)=∫(Fx'*(Gy-Fy)-Fy'*(Gx-Fx))dt-∫(Gx'*(Gy-Fy)-Gy'*(Gx-Fx))dt
c(t)=∫(Fx'-Gx')*(Gy-Fy)dt + ∫(Gy'-Fy')*(Gx-Fx)dt
c(t)=-∫(Gx-Fx)'*(Gy-Fy)dt + ∫(Gx-Fx)*(Gy-Fy)'dt
部分積分の公式より
c(t)=-∫(Gx-Fx)'*(Gy-Fy)dt +[(Gx-Fx)*(Gy-Fy)](a→b)- ∫(Gx-Fx)'*(Gy-Fy)dt
c(t)=[(Gx-Fx)*(Gy-Fy)](a→b)- 2∫(Gx-Fx)'*(Gy-Fy)dt ・・・(1)
この式はこれ以上簡単にならないように思えるが、B-spline曲線はベジェ曲線の集まりであるから各ベジェでこの積分式を解くことができる。
c(t)もB-spline曲線の性質により簡単に求まるので、F(t)とG(t)の関係式が得られる。
関係式が得られたら線分と中点も求まる。
なお辺が交差して四角形が崩れないようにするには大陸間横断線分が他の部分と交差しないように湾を削っておけばよい。

>>598
どんな曲線でもいいわけではなく(1)が解けなければいけない。

600:デフォルトの名無しさん
14/10/23 19:46:13.66 xJ2edcK8.net
>>599
人格障害ですか?お大事に。

601:デフォルトの名無しさん
14/10/23 20:26:31.21 TE8bWo7Y.net
まともに解こうとすると糞難しい。
この問題を安易に解く方法は両陸地に接する円をすこしづつ動かして中心点をつないでいくのがよい。

602:デフォルトの名無しさん
14/10/23 21:45:05.80 lKZXmaCH.net
>>597
離散数学やアルゴリズムの教科書の演習問題みたいなのでいいんだよな。

>>300
>教科書の章末問題をサクサクっとインプリメントすることを目的としてる。
>実用性はあんまり求めない。

603:1
14/10/23 22:11:09.64 gc7yGcGD.net
>>602
>離散数学やアルゴリズムの教科書の演習問題みたいなのでいいんだよな。
おk
できれば言語差がはっきりわかるやつ頼む。

604:587ではない
14/10/23 22:48:38.73 jdc4xe8Q.net
>>597
問題領域が「有限集合と集合間の関係」でモデル化できるのであれば、
関数型やオブジェクト指向よりも論理型言語の Prolog のほうが圧倒的に簡潔に書ける

・プログラミング雑談スレ♯+++
 スレリンク(tech板:357-371番)

この例では、従業員/部門/所属という有限集合を扱っている
たとえば集合 従業員 は以下のように定義される

 従業員 = { <1, 山田>, <2, 鈴木>, <3, 田中>. <4, 松下>. <5, 本田> }

ここで、「<X, Y>」は集合 X と Y の直積を表す

605:デフォルトの名無しさん
14/10/24 11:20:44.18 gLVwzl7v.net
Coqにおける集合論的直観主義 数学の実装
URLリンク(shirodanuki.cs.shinshu-u.ac.jp)

ハイ、このスレ終了~

606:デフォルトの名無しさん
14/10/24 19:07:28.65 smFrq6Ls.net
そういう意味での終了ならとっくに終了してる。ずっと雑談スレとして続いている。
まあこのペースなら放置よりも1000の方が落ちるのが早そうだから、さっさと消化して落としてしまうのがいいだろう。

607:デフォルトの名無しさん
14/10/25 13:59:00.13 hqtmXmou.net
>>605-606
ほんとにCoqなんかで終了と思っとるん?

608:デフォルトの名無しさん
14/10/25 14:49:44.46 CW0KbvIq.net
思ってるよ
何か問題でも?

609:デフォルトの名無しさん
14/10/25 15:00:33.74 rVCkRMh+.net
それは証明系であって、汎用プログラミング言語じゃない。
コーディングしているのは証明。

610:デフォルトの名無しさん
14/10/25 17:23:24.88 0lds8eT1.net
>>609
それのどこが問題なんだ?

611:1
14/10/25 21:33:01.44 ujOd7NYK.net
prologでconnect4作ろうとしたんだがやり方がよくわからん。
盤面の情報はどうやって保持すればいいんだ?

612:デフォルトの名無しさん
14/10/26 04:14:23.56 dhX+3K0L.net
>>611
リストじゃダメなのか?
効率が良くなければならないってことはないんだよな?

>>299
>関数型言語は効率が悪そうたって、「集合論に基づいた言語」とかいうのはもっと効率が悪くなるだろうに。

>>300
>集合論に基づいた言語は教科書の章末問題をサクサクっとインプリメントすることを目的としてる。
>実用性はあんまり求めない。

613:デフォルトの名無しさん
14/10/26 11:52:04.74 WbgAndU6.net
>>612
その人に理由きいたって無駄だよ。
関数型言語は効率悪いから集合論言語として却下するけど、
集合論言語は効率度外視でいいとか言い出す上に
ルビーは文字列操作ユーティリティーが充実してるから使えるとか
真顔で書いちゃう人なんだから。

614:デフォルトの名無しさん
14/10/26 12:19:59.03 lx1fz+FP.net
おいおいそんなこと書くと『わざと曲解してないか?』って言われちゃうぞ

615:1
14/10/26 19:06:58.39 bR5aD7tI.net
>>613
関数型言語却下は効率わるいからじゃなくて生産性あがんないからだよ。
まあ、探せば生産性あがる問題もあるのかもしれんが。

prologなんか無限ループっぽくなるんだが。
裏でなにやってんのかよくわからん。
prolog確かに面白そうではあるんだが、いまいち理解できん。

616:デフォルトの名無しさん
14/10/26 21:24:52.33 cZX7ddvm.net
>>615
有限集合限定でよければHaskellのリストで代用できるだろ。重複要素を取り除くようにすればいいだけで。
「生産性が上がらないからHaskell等は却下」ということなら集合を扱う言語を新たに作っても生産性は上がらない。

1は「集合を扱う言語を作れば高い生産性をもつはずだ」と具体案も示さずに言っているだけ。

617:1
14/10/26 21:39:05.82 bR5aD7tI.net
>>616
リストで集合の代用できるのは確かにそうだが、それを言ったらいろんなデータ構造が無意味になっちゃうだろ。
代用できるだけじゃやっぱダメなんだよ。

具体案を出してないのは認める。

618:デフォルトの名無しさん
14/10/26 22:12:04.35 lx1fz+FP.net
「生産性」とかいいながらやっぱり効率の面で却下してるね
もいっぺん>>615-617を冷静に読みかえしてみて。
>>616は一言も効率(やデータ構造)の話はしてないよ

せめて自分の頭んなかくらい整理して書いてくれ
整理せずに断片的に書きちらしてるから後出しって言われんだよ

619:1
14/10/26 22:24:04.14 bR5aD7tI.net
>>618
俺も効率の話はしてないつもりだったが。
例えばキューやスタックなんかはリストで簡単に代用できるが、
専用のクラスを用意しておくことは意味があると思ってる。

620:デフォルトの名無しさん
14/10/26 22:37:21.48 lx1fz+FP.net
なんでそこでキューやスタックがでてくるんだw
有限集合の話じゃないのかよwwww

621:1
14/10/26 22:40:47.72 bR5aD7tI.net
集合とリストは本質的に異なるという立場。
まあ、代用はできるんだが。

622:デフォルトの名無しさん
14/10/26 22:51:49.39 lx1fz+FP.net
では>>616が書いて>>1も同意したように
"重複要素を取り除く"ような薄いラッパーをかませばhaskellのリストは有限集合の代用になるのに
それ以外に効率とは関係なく「生産性」の上で課題になる「集合とリストの本質的な違い」ってなんだ?

623:1
14/10/26 23:02:30.10 bR5aD7tI.net
ぶっちゃけラッパーかませば問題ないなw
そういう薄いラッパーみたいなこまごまとした小道具がきっちりそろってるのがRubyの魅力だったりする。
でもまあ、今更だけど効率的に計算オーダーが変わっちゃうのはやっぱちょっと気になるかな。

624:デフォルトの名無しさん
14/10/26 23:09:02.90 uNWVyTps.net
Rubyしかしらないだけでしょ

625:デフォルトの名無しさん
14/10/26 23:16:23.07 lx1fz+FP.net
効率以外の面では既存言語(例えばhaskell)に集合操作ぽいラッパーがあればそれで充分と認めたんだよな?
問題は有限集合を扱う効率だけだということになってかなり整理されたな。

じゃお前さんが「生産性」の上では充分だと思うようなラッパーを既存言語の上で定義してくれよ。
haskellでもrubyでもいいよ
それがあれば効率よく処理する必要があるターゲットがみんなにも具体的によくわかる。

626:1
14/10/27 00:02:38.69 hKk3OxSM.net
>「生産性」の上では充分だと思うようなラッパー

ここが一番難しい。
ぶっちゃけ、まだこれだというアイディアはない。

普通に考えると集合論で定義されている一般的な演算をインプリメントすることになるんだろうけど、
それで生産性どの程度あがるかなぁ。

まあ、>>59>>62でも言ってるけど、なんか面白いアイディアがないとダメかなと思ってる。

627:デフォルトの名無しさん
14/10/27 00:16:15.58 xsoB8LA3.net
ここまで短時間で主張を二転三転されると笑うしかないな
あえて好意的に解釈しても正気かどうか心配になるレベル

628:デフォルトの名無しさん
14/10/27 00:50:39.76 UstcwDIj.net
関数型で生産性上がらないみたいなこといってるけど、例えば商集合演算を書く時はどうすんの。
集合論に基づいた言語を作るなら、少なくとも関数がファーストクラスであることは生産性に大きく関わると思うんだけど。
あと数学の関数は状態を持たないから、全ての関数が参照透明であるかどうかはともかくとして、
数学の意味での関数を使う場合には参照透明な関数であることを制約するような記述ができる必要があるかもね。

629:デフォルトの名無しさん
14/10/27 03:06:19.81 S1pbHk8f.net
>>623
「集合論に基づいた言語」を新たにつくっても、その言語に「こまごまとした小道具」はそろってないわけだが、
そうするとその新言語は1にとって魅力がないってことになるんじゃないか?
Rubyだったら簡単にできることが新言語では簡単にはできないのだから。

630:デフォルトの名無しさん
14/10/27 04:05:38.32 dHQizD3i.net
>>420
>>409のリンク先にあるような、集合や列の内包表記を使ったプログラムを読むのは1にはしんどいってことだな。

631:デフォルトの名無しさん
14/10/27 05:43:19.35 Rvvlh30F.net
結局、ルビー以外を提案しても全部却下して
「ここがルビーのいいところ」とか書いちゃうんだよ。
関数型言語の生産性の高さも知らずにね。

632:デフォルトの名無しさん
14/10/27 06:55:54.77 9dCb0Lih.net
そもそも「作りたい」ってスレタイが間違ってんじゃね
こいつ絶対作る気ないだろ

633:デフォルトの名無しさん
14/10/27 11:42:55.16 VoSGhOqg.net
そんなことはどうでもいい

634:1
14/10/27 20:16:20.56 hKk3OxSM.net
>>627
まあ、確固たる主張があるわけではないからな。

>>628
関数はファーストクラスの方がいいだろうな。
参照透明性は微妙。
あるに越したことはないけど、そこ頑張りどころかなぁ?という気はする。

>>629
ぶっちゃけ、Rubyは最強言語なので。
そんな簡単には超えられないでしょう。

>>630
正直、かなりしんどい。
あれ以上は簡単にできないのかもしれんが。

>>631
関数型言語で生産性が上がる問題があるなら教えてくれ。

>>632
まだネタ出しの段階だからな。実装ははるか先の話だ。

635:1
14/10/27 20:19:14.66 hKk3OxSM.net
それにしてもprolog動かんなぁ。
センスないわ俺。

636:デフォルトの名無しさん
14/10/27 21:05:20.40 K1rstjve.net
>>634
>関数型言語で生産性が上がる問題があるなら教えてくれ。

で、相手が何か例を挙げたらケチつけるんだろw
自分は「集合論に基づいた言語」で生産性が上がる例を示さずにw

637:1
14/10/27 21:22:05.89 hKk3OxSM.net
俺がケチつけられないほど明確に生産性の上がってる問題を頼む。

638:1
14/10/27 21:25:15.63 hKk3OxSM.net
まあ、集合論に基づいた言語は絵空事で終わる可能性があるからな。
関数型言語はそんなことないんだろ?

639:デフォルトの名無しさん
14/10/27 21:40:34.27 xsoB8LA3.net
ほんとに何言ってんのかねこの人はwww

640:デフォルトの名無しさん
14/10/27 21:48:32.99 K1rstjve.net
>>637
そうした例を挙げても1に餌を与えるだけだし。
関数型言語でも論理型言語でもその他でも同じこと。

641:デフォルトの名無しさん
14/10/27 22:01:34.98 UstcwDIj.net
高階関数によるチェインなんかは生産性のあがる例じゃないの。並列化も簡単でしょ。
まあ関数型のスレではないけど、集合論というか数学ってまさに関数型言語なのに、
よくわかってなさそうだからつっこまれるんだろうけど。

642:デフォルトの名無しさん
14/10/27 22:37:28.46 K1rstjve.net
>>300
>集合論に基づいた言語は教科書の章末問題をサクサクっとインプリメントすることを目的としてる。
>実用性はあんまり求めない。

>>305
>集合論に基づいた言語では狭い領域の問題に限り(教科書の章末問題とか)
>高い生産性を発揮することを目標にしてる。

「サクサクっとインプリメント」できるどうか、「高い生産性を発揮」しているかどうかは、1の主観で判断される。

643:1
14/10/27 22:42:25.97 hKk3OxSM.net
>>641
確かに高階関数はカッコいい気がするが、具体的にどんな問題で使われてるか知らない。
並列化は簡単というが、まだ実現はしてなかったような。
まあ、俺は関数型言語も数学も造詣はないな。

644:デフォルトの名無しさん
14/10/27 22:54:12.79 CRLCLkYm.net
jqueryのメソッドチェーンは便利だね

645:デフォルトの名無しさん
14/10/27 22:57:50.25 UstcwDIj.net
>>643
個人的な経験でいえば、DBからデータを取ってきて加工したりするときに非常に書きやすいかな。
とにかく、コレクションのデータを加工して流すときに非常に簡潔に書ける。
他にもあるけど、今すぐに思いついたのはこれかな。
並列化はClojureなんかは簡単に書ける。Javaも8からできたんじゃなかったっけ。まあJavaのあれは関数型と言うには気持ち悪いけど。
というか、適用する関数が副作用を持たないと仮定するなら、作用させるデータを分割して再結合すればいいっていう単純な話でそ。

646:デフォルトの名無しさん
14/10/27 23:02:23.54 UstcwDIj.net
あ、メソッドチェーンにおける並列化が簡単にできるという意味ね。
プログラム自動並列化は詳しくないけどまだ発展途上じゃないかな。

647:1
14/10/27 23:32:47.45 hKk3OxSM.net
>>645
ふーむ。確かにコレクションのデータを加工して流すのは出現頻度が高そう。
勉強になりました。
Clojuerちょっとぐぐってみたけど、ソフトウェア・トランザクション・メモリーとかよくわからんかった。
とりあえず簡単に並列化できそうな雰囲気は伝わってきたw

648:デフォルトの名無しさん
14/10/28 00:54:20.05 2moDL6+C.net
>>とにかく、コレクションのデータを加工して流すときに非常に簡潔に書ける。
>ふーむ。確かにコレクションのデータを加工して流すのは出現頻度が高そう。
>勉強になりました。

このスレでHaskellの名前が出てから2ヶ月たつけど、2ヶ月の間に自分で調べたりはしなかったんだな。

649:デフォルトの名無しさん
14/10/28 01:22:16.19 F9KmtOQp.net
この言語が最強っていう信念のある人だからね

650:デフォルトの名無しさん
14/10/28 01:46:36.67 2moDL6+C.net
Ruby最強と思っているらしいけど、それなら新しい言語を作ろうなんて思わければ良さそうなものだがな。
新しい言語を作っても、Rubyにあるような、お気に入りの便利な機能なんかないから、「Rubyなら簡単にできるのに」
って不満がたまるだけだろうに。
集合を使った表記法のプログラムを読むのもかなりしんどいそうだし。>>634

651:デフォルトの名無しさん
14/10/28 13:51:55.51 /Y9XnqU0.net
>>638
ちょっと待った。
絵空事で終わらない可能性がゼロでないことを説明してくれ。

>>643
C++ やるんじゃなかったけ? <functional> とか高階関数だらけじゃん。
Javascript とかでも良く使うよ。Ruby では使わないの?

652:デフォルトの名無しさん
14/10/28 14:27:02.71 BaOL+HSr.net
>>643
高階関数って名前じゃ無くても同じ事させてるのは体験してるだろ?
あるオブジェクトのリストを(必要な要素だけ抽出(filter)してデータ変換(map)して集約(reduce)させるとか

653:デフォルトの名無しさん
14/10/28 15:52:04.32 g7PPMDyH.net
関数型の生産性の証拠は求めるけど
もちろんルビー最強の証拠なんて知らんぷり

654:デフォルトの名無しさん
14/10/28 15:53:32.28 g7PPMDyH.net
典型的なルビ厨

655:デフォルトの名無しさん
14/10/28 16:20:55.17 mPN7Yd+C.net
>集合論に基づいた言語は教科書の章末問題をサクサクっとインプリメントすることを目的としてる。
>実用性はあんまり求めない。

>集合論に基づいた言語では狭い領域の問題に限り(教科書の章末問題とか)
>高い生産性を発揮することを目標にしてる。

1の言う「生産性」はこういうことだから、教科書やそれに載ってる問題を具体的に挙げて、
この問題をこういうふうに書きたいんだけど、Rubyではこんなふうにしか書けない、
Haskellではこんなふうにしか書けない…、そのためにサクサクっとインプリメントすることができず、
生産性が上がらない

って話を1がしないとどうしようもないんだよな。
Rubyその他、既存の言語で「サクサクっとインプリメントすること」ができるのなら
新しい言語をつくる意味がないんだから。

656:デフォルトの名無しさん
14/10/28 20:20:01.18 sNcgfmnM.net
>>655
結局それにつきるな
それに対して1は具体的はアイディアがないからとか
返答になってないことをうだうだ言うだけで問題意識を明らかにしようとはせず
そのうちまた新しいループがはじまる、と。

657:1
14/10/28 21:27:06.97 Eyw4r4/G.net
>>648
まあな

>>651
>絵空事で終わらない可能性がゼロでないことを説明してくれ。
それはむずかしいな。
数学っぽくプログラムできたらいいんじゃね。とか
教科書の記述がそのまま実装になったらいいんじゃね、とか
そういう曖昧なイメージがあるだけで、見切り発車でスレたてたからな。

>C++ やるんじゃなかったけ? <functional> とか高階関数だらけじゃん。
functionalって使ったことないかも。
setやmapでoperator<を定義することはあるけどそれとは違う?

>Ruby では使わないの?
Enumerableのメソッドならよく使うが。

>>652
Rubyのcollectとかはよく使う。

>>655
>>656
まあ、サクサクインプリメントできない問題が具体的にあったわけじゃないんだよな。
数学的な記述がそのまんま実装になったら楽しいかなぁとかその程度の問題意識しかなかった。
プログラミングの素養がなくても教科書丸コピで動いちゃうみたいな?
そんな感じ。

ちなみに、教科書丸コピは後付けなんだよなぁ。
いろいろやってるうちにこのスレを立てた時の最初の気持ちは何だったのかもう忘れてしまった。

658:デフォルトの名無しさん
14/10/28 22:13:27.20 SAcW2ukT.net
>>657
教科書の演習問題を丸コピすれば答を出してくれるソフトをつくろうと
してたのか? w

ごまかそうとしないで、どの教科書のどの演習問題をどのように実装できる
言語をつくろうとしているのかちゃんと書け。

659:デフォルトの名無しさん
14/10/28 23:02:45.22 SAcW2ukT.net
>>575
こんなことを書くぐらいだから、推論や数式処理の機能をもつ言語を考えていたわけじゃないよな。

660:デフォルトの名無しさん
14/10/29 01:09:17.84 7WbuvXm2.net
プログラミング言語に有限集合を扱う機能を持たせさえすれば
離散数学やアルゴリズムの教科書の
「数学的な記述がそのまんま実装になった」り
「プログラミングの素養がなくても教科書丸コピで動」かせるようになると
1は思っているということだな。

661:デフォルトの名無しさん
14/10/29 07:51:54.82 uFHhP6NK.net
>>657
>数学っぽくプログラムできたらいいんじゃね。とか

いい言語を教えてやろう。FORTRAN (FORmula TRANslator) だ。

662:デフォルトの名無しさん
14/10/29 15:03:48.76 +dOdWCkt.net
>>655
ヤフーニュースのコメント欄の私もそう思うボタンを探してしまった。

>>657
> setやmapでoperator<を定義することはあるけどそれとは違う?
std::set<int, std::less<int> > s;
const size_t c = std::count_if( s.begin(), s.end(), std::bind2nd(std::greater<int>(), 5) );
例えば後者。関数を返す関数を呼んで、戻された関数を別の関数が呼んでる。

663:デフォルトの名無しさん
14/10/29 20:53:26.55 0HNaGJ1I.net
当の本人がどうしたいのかハッキリしてない以上
「顧客が本当に必要だったもの」のあの絵の状態になる可能性は非常に高い
本人はプログラマのつもりかも知れんが、実際は顧客の物言いをしてる
しかも、注文とダメ出しだけ多くて、かつ本人は解ってる(つもり)というタイプの

この板は「こんなソフト作ってよ」と頼む場所ではないと思うのだが

664:デフォルトの名無しさん
14/10/29 21:05:16.16 ITcKex6d.net
まだ構想(=夢)の段階であれこれと夢想し構想し、その過程が文字で見える過程を、傍からみている私は楽しんでいる
>>1 続けてくれ

665:1
14/10/29 23:04:45.80 6KDieIbJ.net
>>658
むりぽ

>>662
bind2ndとか知らなかったわ。テンプレート恐るべし。
まあ、勉強になりました。

>>664
ぶっちゃけ、毎日書き込むのつらくなってきたわ。
このスレは今後不定期更新になりますw

666:デフォルトの名無しさん
14/10/30 00:38:38.53 HxKeCYce.net
>>665
1が書き込んだあとには

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

と書いたほうがいいな。
そうしないと同じことの繰り返しになるだろうから。

667:デフォルトの名無しさん
14/10/30 03:27:37.45 sggd5tBz.net
>>666

>>425も追加で。

668:1
14/10/31 20:03:03.95 g6D744er.net
prologのconnect4がどうしても動かん。
誰か俺のコードをデバッグしてくれ。現状のコードは以下。
get_atでリストのN番目の要素を返す。
get_stoneでBOARDの(X,Y)の位置にある石を返す。盤の外を指定したときは3を返す。
straightで連続した石の数を数える。DX,DYは連続した石を探索する方向。

board([[],[],[],[],[],[],[]]).
myboard([[1,2],[1,1],[1,1,1],[1,1,1,2],[],[],[1,2,1]]).
get_at(_,[],_):- fail.
get_at(0,[X|_],X).
get_at(N,[_|Ls],Y):-
N1 is N -1,
get_at(N1,Ls,Y).
get_stone(_,X,_,3):- X<0,!.
get_stone(_,X,_,3):- 6<X,!.
get_stone(_,_,Y,3):- Y<0,!.
get_stone(BOARD,X,Y,0):-
get_at(X,BOARD,Xs),
length(Xs,L),
Y >= L,!.
get_stone(BOARD,X,Y,S):-
get_at(X,BOARD,Xs),
get_at(Y,Xs,S),!.
straight(BOARD,X,Y,_,_,S,0):-
get_stone(BOARD,X,Y,S1),
S1 \== S,!.
straight(BOARD,X,Y,DX,DY,Stn,Len):-
X1 is X + DX,
Y1 is Y + DY,
Len1 is Len + 1,
straight(BOARD,X1,Y1,DX,DY,Stn,Len1),!.

669:デフォルトの名無しさん
14/10/31 20:34:56.87 eFG4AR46.net
>>668
それと「集合論に基づいた言語を作る」のとどういう関係があるんだ?

>>666-667

670:デフォルトの名無しさん
14/10/31 20:42:19.57 eFG4AR46.net
>>668
↓で教えてもらえ
【論理】Prolog【初心者】
スレリンク(tech板)

671:デフォルトの名無しさん
14/11/01 00:21:10.18 QdACbqof.net
>>670
その結果。

スレリンク(tech板:786番)
|全般的な感想として、1)..3) を見るに (Prolog 以前に)一般的なプログラミングの基礎が身に付いていないと思う
|おそらく集合理論言語スレの 1 だと思うけど、大学で情報系を専攻していたのなら情けない結果だ
|学生時代に遊んでいたのか、当時はできたけど今はその感覚が戻っていないだけなのか、わからないけどね
|現状のレベルでは、言語処理系を自作するなんてのは、夢物語か妄想のたぐいと判断せざるをえない

672:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/11/01 20:55:00.77 jtBHZTX6.net
Boost.Iclを参照せよ。

673:1
14/11/02 00:06:07.92 WfQoOxnP.net
>>672
情報はありがたいんだが、レスするのペースダウンするつもりなので宿題にさせてくれ。

674:デフォルトの名無しさん
14/11/02 14:33:07.98 2+jwxmIt.net
>>673
>宿題

集合論に基づいた言語の作成に関係があるからこのスレに書くべきだと示せるのでなければ
宿題はBoost総合スレにでも行ってやれ。
Boostに興味がある人・詳しい人はそっちのスレのほうが多くいるはずだ。
他の言語・ライブラリのことでも同様。その言語・ライブラリに興味がある人・詳しい人が多そうなスレを選んで書け。

>>425 >>559 >>655-665

675:1
14/11/02 18:33:09.61 WfQoOxnP.net
>>674
このスレの基本スタンスは雑談なので面白そうなトピックスは適宜拾っていったらいいんだぜ?
そうじゃなきゃ尺が稼げんだろうがw

676:デフォルトの名無しさん
14/11/02 20:08:03.24 4mhasaGI.net
>>425
今度は『ここは雑談スレだ』と言い出した。

677:1
14/11/02 21:55:00.94 WfQoOxnP.net
あと、このスレは俺中心に進めていく必要はないんだぜ?
みんなで雑談してくれて構わないんだぜ?

678:デフォルトの名無しさん
14/11/02 22:45:12.36 2oaHueQb.net
>>676
雑談スレはすでにあるのにな。
スレリンク(tech板)

>>559
1は「何でもいいから話題クレクレ」に路線変更。

679:デフォルトの名無しさん
14/11/03 08:07:42.94 FKymKC8X.net
>>1
> 徹底的に集合論的思想で言語仕様を考えるスレです。

どう読んでも雑談スレじゃないよね

680:デフォルトの名無しさん
14/11/03 11:16:05.33 C9Z/RfTt.net
それでもいいんじゃない‥雑談スレはすぐに話題が収束するからね‥

681:1
14/11/05 21:01:40.21 aXYuBMMC.net
prolog版connect4できたっぽいのであげます。
URLリンク(www.age2.tv)

長かった…!
prologでプログラミングするには…
なんと多くの辛抱が必要なものかと…!

あんまりテストしてないのでバグがあるかも。

682:1
14/11/05 21:29:06.77 aXYuBMMC.net
prolog識者がいたら添削たのむ

683:デフォルトの名無しさん
14/11/06 01:04:11.78 i9pGGwTT.net
>>681-682
>>669-670
>>425 >>559 >>655-665

684:デフォルトの名無しさん
14/11/06 01:47:04.84 TxZPnLvK.net
>>682
TwitterにPrologおじさんがいるからみてもらえ

685:1
14/11/06 20:03:55.57 1yGaI9pi.net
>>454
>>456
>>587
なんかコメントくれ。

>>684
Prologおじさんてその道で飯くってるひとじゃね?
こちらからタダで見てくれとは頼みづらいわな。
お前らみたいに自発的にスレ見てくれてる人とは訳が違う。

686:デフォルトの名無しさん
14/11/06 21:01:27.80 C8/OFtDI.net
>>685
>>454 >>456 >>587の3人にコメントを求める前に>>655-665。

1はプログラムを添削してほしいのに添削できる人が集まってそうなところを避けるようなバカだしな。

687:1
14/11/06 22:26:58.78 1yGaI9pi.net
Boost.Iclちらっとぐぐってみたけど、実装の大変さの割に活躍する場面があんまりないようなw
いつ使うかな~コレ。
たしかに集合っちゃ集合なんだけど正直微妙。

688:デフォルトの名無しさん
14/11/07 04:13:14.72 QM030TJs.net
>>685
>>1の「クレクレ」が不快だと言っている>>587に対してコメント「クレクレ」w

689:デフォルトの名無しさん
14/11/07 04:36:31.62 Nfw1pK0/.net
>>454 >>456 >>587が言ってるのは「集合論に基づいた言語」を作るのならPrologが参考になるはずということだろうから、
1がPrologで書いたプログラムにコメントしなけりゃいけないというものではないな。

690:デフォルトの名無しさん
14/11/07 17:32:05.33 eCqmNoes.net
実装が大変かどうかは問題にならん。

691:1
14/11/07 20:05:41.11 FWyIh5H/.net
>>690
まあ、ユーザーからすれば問題にならないけど。
Boostの人たちももうやり尽しちゃったて感じかなw。

692:デフォルトの名無しさん
14/11/08 05:55:33.54 N89Y1+Fh.net
これが集合論の何に参考になるのかサッパリわからんわ。
添削するだけ無駄。結局文句だけ言ってルビー最高って結論出すだけw

693:1
14/11/08 10:50:24.96 vsjOn1b1.net
>>692
おれもサッパリわからんわw
文句は>>454 >>456 >>587に言ってくれ。

prologでconnect4作ってみて思ったのは
connect4は習作として優れているってことと、
prologはconnect4作るのに向いてないってことだなw

prologでプログラム組むにはかなり慣れが必要。
ぶっちゃけ特殊技能やなこれ。
発想は面白いとおもうがこれで真面目にプログラム組もうと思う人がどれだけいることか。

しかし、prologの変数は参照透過なのかな。
haskellよりプログラム書きづらかったわ。

まあ、Ruby最強だな。

694:1
14/11/08 12:45:40.20 vsjOn1b1.net
×connect4は習作として優れている
○connect4は習作の題材として優れている

695:デフォルトの名無しさん
14/11/08 15:02:48.96 PXfop+Ut.net
>>693-694
>>300
>集合論に基づいた言語は教科書の章末問題をサクサクっとインプリメントすることを目的としてる。
>実用性はあんまり求めない。

connect4は、どの教科書の章末問題なんだ?

696:デフォルトの名無しさん
14/11/08 15:17:42.64 N89Y1+Fh.net
connect4を集合論プログラミングの例題として使いたいんなら、
まずはconnect4のルールを集合論的に定義するのが先だ。

今のところ1がやってるのは単なる手続き的実装例の移植じゃん。
それで参考になるわけがない。

697:デフォルトの名無しさん
14/11/08 15:33:25.11 oJ3Se8B2.net
>>695
「教科書」は「離散数学とかアルゴリズムのやつ>>523」か集合論のものに限定。
挙げられなければ、また1の後出しジャンケンってことで。
>>425 >>559 >>655-665

698:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/11/08 15:40:24.89 ebCh2W7f.net
記述は日本語なのか英語なのか数学記号によるのか?

699:1
14/11/08 19:44:24.22 vsjOn1b1.net
>>695
connect4が載ってる教科書は見たことないな。

>>696
>>697
connect4は新しい言語を勉強するときに都合がいいから使ってるだけであって、
集合論プログラミングとは関係ないんだけどな。
というか、集合論プログラミングの題材としてどんなものがいいかは
まだよくわかってないんだよな。
正規言語とオートマトン、文脈自由言語とプッシュダウンオートマトン
あたりかなぁとは思っているんだが。

>>698
数学記号じゃね?

700:デフォルトの名無しさん
14/11/08 19:53:04.25 LHO3gvAT.net
>>693
プログラミングパラダイムごとに得意な領域、不得意な領域が存在するのに、なんで例題一個だけで言語を判断しようとするの?短絡的すぎない?
全部Prologで書くのはきついものがあるけど、部分的にPrologを採用してるプロジェクトはあるよ
(とはいえPrologがconnect4を作るのに向いているかどうかで言えばたぶん向いてないとは思うけどね)

701:1
14/11/08 20:18:34.70 vsjOn1b1.net
>>700
ぐう正論ですな。
まあ、そんな簡単に新しい言語は深く習得できないからな。
感触掴むくらいがせいぜいじゃね?
判断が早いというのは言われてみればそうだと思う。
ちなみにPrologで生産性が上がる問題があるなら教えてくれ。

702:デフォルトの名無しさん
14/11/08 21:02:07.77 7W78geqS.net
>>699 >>701
>集合論プログラミングとは関係ない

ならPrologスレでやれよ。
Prologに詳しい人はそっちのほうが多いはずだ。

【論理】Prolog【初心者】
スレリンク(tech板)

703:1
14/11/08 21:21:57.05 vsjOn1b1.net
connect4は直接関係ないけどprologは関係あるかもしれないだろ。
つか、なんでこのスレでやっちゃダメなんだ。
意味わからん。

704:デフォルトの名無しさん
14/11/08 21:29:37.77 7W78geqS.net
>>703
>なんでこのスレでやっちゃダメなんだ。

スレ違いだから。

Prologの勉強をPrologスレでやってみて、「集合論に基づいた言語の作成」に関する話になったらここに来ればいい。

705:デフォルトの名無しさん
14/11/08 21:35:40.48 LHO3gvAT.net
>>701
まあ実を言うとPrologについてそんなに詳しくはないので、文法とWIkipedia程度の知識しかない
歴史的には定理自動証明の分野で使われてきていて、
最近ではIBMの例のワトソンのコアに使われてたりするとか、まあやっぱ知識処理なのだろうか
あとユニフィケーションと並列化の相性がよく、派生言語がいくつか出てるらしいね、Erlangとか
>>702のスレも業務への適用の話とかしててまだ途中だけど読んでて結構おもしろい

まあ言いたかったことは、他のパラダイムは切り捨てるより取り入れたほうが自分の糧になるよということで
以前関数型あたりも簡単に切り捨ててたから、それじゃもったいないよ

706:1
14/11/08 21:55:42.68 vsjOn1b1.net
>>704
You can't connect the dots looking forward. You can only connect them looking backwardsだよ!

>>705

>あとユニフィケーションと並列化の相性がよく、派生言語がいくつか出てるらしいね、Erlangとか

ErlangってPrologの派生だったの?
なんか並列化が得意らしいというのは聞いたことがあったが。

> >>702のスレも業務への適用の話とかしててまだ途中だけど読んでて結構おもしろい

そういやPrologスレちゃんと読んでないな。読んでみるか。

>まあ言いたかったことは、他のパラダイムは切り捨てるより取り入れたほうが自分の糧になるよということで
>以前関数型あたりも簡単に切り捨ててたから、それじゃもったいないよ

またまたぐう正論ですな。
気を付けます。

707:デフォルトの名無しさん
14/11/09 06:16:58.35 co8RBkg8.net
>>706
だーかーらー、そのconnect4とやらのルールを集合論的に書けばいいって言ってるだろ。
さっさとやれ。

708:デフォルトの名無しさん
14/11/09 16:46:55.86 9LyR+5oz.net
1は何かものを作れる人間じゃないから。

709:1
14/11/09 18:17:59.58 Yrjok8yA.net
>>707
んーどうだろうな。
俺もスレたてた時はすべてを集合で表せば数学的にうまくいくんじゃね?とか思ってたんだけど、
やっぱリストはリスト、タプルはタプルなんだよな。
connect4も無理に集合的に扱わないで手続型で扱った方が自然かもしれないんだよな~
ぶっちゃけ、集合にこだわる意味が根底から揺らいでるw
数学の基礎的な部分が集合論でできてるってのはそうなんだろうけど、
応用問題解くときに些末な問題に煩わされたくないよね?

まあ、集合論でうまくいきそうな問題⇔教科書の章末問題かなぁとか思ってたんだけどさ。
その辺はあんまり整理できてない。

710:デフォルトの名無しさん
14/11/09 19:17:53.75 co8RBkg8.net
リストもタプルも集合論の枠組み内で普通に扱えるのだが、
もういいや、1に何かを期待するのはやめた。

711:デフォルトの名無しさん
14/11/09 19:30:26.31 FyV/3PpB.net
そろそろループ再開ですか?

712:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/11/09 19:44:15.77 XU91kGr5.net
算術演算+-×÷!/√
括弧()[]
等号不等号=≠<>≦≧≒≪≫
無限大∞
集合∈∋⊆⊇⊂⊃∪∩{|}#
論理:∧∨¬⇒⇔∀∃→∴∵
パーセント%
その他の記号±≡…;?

713:デフォルトの名無しさん
14/11/09 20:00:10.30 NPL58Du1.net
1に餌を与えないでください。
>>425>>559 >>655-665

714:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/11/09 20:28:33.70 XU91kGr5.net
俺の研究内容が似ているので燃料投下する。国の生活保護と同様に、たとえ悪魔にもエサを与えよう。

715:デフォルトの名無しさん
14/11/09 21:17:29.34 b4iNH/wh.net
1「悪魔の餌 クレクレ」

716:1
14/11/10 21:45:18.40 AsAdiTVl.net
試しにRubyでconnect4書いてみた。
URLリンク(www.age2.tv)

行数的にはhaskellのほうが短いくらいなんだが^^;
オフサイドルールのせいかな?

717:デフォルトの名無しさん
14/11/11 04:23:27.89 m7WVeZhS.net
>>716
スレ違いだバカ

718:デフォルトの名無しさん
14/11/11 16:25:56.08 kmmZIWoZ.net
スレタイでHaskellで良いじゃんと思ってスレ開いたら1が馬鹿すぎてスレをそっと閉じることにした

719:1
14/11/17 21:47:20.82 IjeD6lYX.net
とりあえず、次の宿題は圏論かな~?

720:1
14/11/17 23:26:02.06 IjeD6lYX.net
とりあえず、ここ読んだけど。。。

URLリンク(ja.wikibooks.org)

ぃみゎかんなぃ。。

もぅマヂ無理。。

リスカしょ・・・

ようするにdoが使いたいだけ?

721:デフォルトの名無しさん
14/11/18 00:04:28.78 e4RrhwW3.net
>>720
Haskellスレでやれ。
Haskellに詳しい人はそっちのほうが多いはずだ。

関数型プログラミング言語Haskell Part26
スレリンク(tech板)

722:デフォルトの名無しさん
14/11/18 00:07:08.02 l6oqTr0E.net
1に餌を与えないでください。
>>425 >>559 >>655-665

723:1
14/11/18 21:56:19.27 +WEtmfNy.net
URLリンク(d.hatena.ne.jp)
ここも読んでみたけどやっぱわからん。
というか、読んでも目が滑る。
だれか圏論のいい入門textプリーズ

724:デフォルトの名無しさん
14/11/19 19:50:12.10 dm216OYo.net
とりあえず『圏論の基礎』でも読んでみたら?

725:1
14/11/19 19:56:54.80 V2tDw9NJ.net
URLリンク(www.amazon.co.jp)
これ?
まあ本屋いってみてあったら立ち読みしてみるわ。

726:1
14/11/26 20:02:22.17 JT4BoUXj.net
圏論の基礎買ったけど早くも積読w

727:デフォルトの名無しさん
14/11/29 18:24:47.22 8AtyRUwF.net
>>701 の話だけど、ドコモで prolog が動いてる的な記事をなんかで読んだことがある

728:1
14/11/30 19:47:48.77 O0/vTNqA.net
URLリンク(iiyu.asablo.jp)
これか。
コード量10分の一は確かにすごい。
しかし2370万行とか正気の沙汰じゃないな。

729:デフォルトの名無しさん
14/11/30 22:28:37.23 mFsly3WX.net
Prolog で書くと「コード量10分の一」となる例には、他にも型推論があるね
以下のblog記事では、単純な型推論をPrologで記述している
・Prolog で型チェック:Rainy Day Codings:So-net blog
 URLリンク(rainyday.blog.so-net.ne.jp)

自分の知る範囲では、世界で最も簡潔な型推論の実装コードだね
これも、もし(型システムという)形式的なルールが定義されていれば、
それを直接的に表現できるという Prolog の特徴が活かされている
Haskell でもこんな芸当はできない

730:デフォルトの名無しさん
14/12/01 15:16:30.87 pglWaPo9.net
おおっと、Haskell信者に対して挑発だ~!

731:デフォルトの名無しさん
14/12/01 15:51:58.42 oEpuqve5.net
別にユニフィケーションがどっち方向にも働く、というのはPrologの特性だし、
Haskellにそんなものあっても困るだけだし。

732:1
14/12/01 19:25:13.06 TTRJBgwa.net
>>729
ふーむ。Rubyだとどうなるかな~。
ヨクワカラヌ。

733:デフォルトの名無しさん
14/12/01 20:27:28.82 pmQ3LQ8v.net
Prologのシンボル使ったユニフィケーションを実装するのは
Rubyに限らず手続き型言語ではライブラリ頼りでやらんと面倒い
むしろそれに特化され過ぎて、手続き的な書き方が面倒いって言語がProlog

734:デフォルトの名無しさん
14/12/01 22:36:56.45 oEpuqve5.net
そういったものをなんでもまぜこぜできるからLispは偉い、というのが
竹内先生@NUEの主張だったなw

735:デフォルトの名無しさん
14/12/01 23:52:04.88 6Gpd+bqZ.net
1に餌を与えないでください。
>>425>>559 >>655-665

1は推論や数式処理を扱うのは面倒くさいと思っている。
>>574-576

736:デフォルトの名無しさん
14/12/02 00:14:21.85 +stn5l+y.net
集合論だと逐次処理やりにくいしな
SQLとも違うみたいだし

737:デフォルトの名無しさん
14/12/03 15:47:19.25 C/BNzxz3.net
集合論だと、逐次処理は処理系の中でやる。
プログラムにはmapやらfilterやらが出てきて、逐次処理は隠蔽されるのでは?

それを考えると、1がlispで満足できないのが不思議でならない。

まぁ、文字通り「何も」考えていないのだろうな。

738:1
14/12/03 19:55:52.44 oIRBJSMm.net
lispってそんないいかなぁ。
ちょっとやったことあるけど、インデントつけても括弧の対応がすぐわかんなくなるんだが。
コード読みにくいったらありゃしない。

739:デフォルトの名無しさん
14/12/03 20:36:17.67 HSbdY3zj.net
>>738
ちょっとやってみただけで慣れようともせずケチつける。
>>700>>701>>705>>706

740:デフォルトの名無しさん
14/12/03 21:18:09.35 DVPNx2yH.net
>>734
S式を使っているからうまく混ぜられる、S式こそLisp最大の特長、とかいう主張だったな。

741:1
14/12/03 22:35:36.35 oIRBJSMm.net
>>740
詳しく

742:デフォルトの名無しさん
14/12/03 23:15:45.16 cePlsLqN.net
ほげ言語のパラドックスでも読んどけ

743:デフォルトの名無しさん
14/12/04 01:08:18.94 jHjIGczB.net
集合に順序があるのはむしろベクトルかタプルに見える

集合論って考えは好きだけどソートみたいな逐次処理でよく使うものはどうなるんだろうか
並列処理的なこと考えてるひとがいるみたいなんでそれに乗っかると
並列処理ならクイックソートよりマージソートのほうが速そうだがそれが集合論かと言われるとちょっと困る

でもソートが本来のやりたいことではなくてソートしたデータにまた何らかの処理をする要求のほうが多い気がするんでどうでもいいか
2分探索なり逐次処理の環境で考えだされたアルゴリズムはほとんど使えない気がするんでまた誰かが良さそうな手順を考えださないとな

744:デフォルトの名無しさん
14/12/05 09:26:36.60 I64sWIzc.net
数学できる人間に見られたいクズが集まるスレ

745:デフォルトの名無しさん
14/12/05 11:54:06.72 IjAdRY0C.net
自己紹介か?

746:1
14/12/05 20:20:24.20 b89FafAC.net
とりあえず、圏論からは戦術的転進するか。
別のネタを探そう。

747:デフォルトの名無しさん
14/12/05 20:55:48.99 B18WNnFt.net
1に餌を与えないでください。
>>425>>559 >>655-665

748:デフォルトの名無しさん
14/12/05 23:22:33.28 oLmzY7WJ.net
しかしまあスレタイ通りにはなかなかいってないけど総合的には良スレっぽい

749:デフォルトの名無しさん
14/12/06 01:07:31.28 tjNXDvF3.net
>>746
圏論を勉強する気など最初からなくて、ネタのつもりだったわけだ。
圏論以外に何をもってきても同じだろうな。

750:デフォルトの名無しさん
14/12/06 10:37:54.51 kt8GWotW.net
lisp の括弧は rainbow-parentheses 的なの入れるとマシになる

751:デフォルトの名無しさん
14/12/06 18:03:11.24 KgmhP8S/.net
lispで区切りに()だけ使うんじゃなくて集合を表す時は{}使うとかどうなの?
集合は{

752:1
14/12/06 18:04:03.49 KgmhP8S/.net
途中で書き込んじゃった。
集合は{}で表すってイメージあるんだけど。

753:デフォルトの名無しさん
14/12/06 18:56:15.26 dXBvUp0m.net
clojureは#{}が集合のリテラルとしてある
他のlispでもリードマクロかけばそういうことはできる
是非についてなら。その表記が存在することが対象のプログラミングに有効ならあり、そうでなきゃなし

754:1
14/12/06 18:59:55.68 KgmhP8S/.net
ほほう。
clojure検討してみる価値あり?

755:デフォルトの名無しさん
14/12/06 19:20:33.09 dXBvUp0m.net
まあlisp系はマクロ書けば簡単に構文拡張できるから、新しい言語を試行錯誤したいなら最適ではあるよ

756:デフォルトの名無しさん
14/12/06 19:20:42.39 5oGFUyw+.net
RubyとかJavaにもSetオブジェクトはあるし、リテラルの有無はソースコードの見た目の問題で、
たいして重要じゃない。

757:デフォルトの名無しさん
14/12/06 19:28:14.31 dXBvUp0m.net
マッチョすぎワロタ
数値や文字列リテラルのない言語でも頑張ってくれそう

758:1
14/12/06 19:49:14.64 KgmhP8S/.net
リテラルの有無は結構気になるな、俺は。
Rubyの配列やマップのリテラルは気に入ってる。

759:1
14/12/06 19:51:57.69 KgmhP8S/.net
clojureってjavaなのか。
クラスパスとかあんまわかってないんだよな~じつは

760:デフォルトの名無しさん
14/12/06 20:40:46.96 VB5mtD/4.net
>>748
VIPやシベリアだったらな。

761:1
14/12/06 21:05:36.24 KgmhP8S/.net
パッと見common lispよりclojureのほうがオサレにみえる。
あんまりcommon lisp知らんけど。

762:デフォルトの名無しさん
14/12/06 21:16:11.69 5oGFUyw+.net
なんでもいいから手を動かせ

763:1
14/12/07 00:04:16.45 2ooQYugx.net
OO言語だとobj.method(x)って書くけどlisp系だと(method obj x)って書くじゃん?
OO言語になれてるからかこの順番の違いが結構イラつく。

764:デフォルトの名無しさん
14/12/07 00:11:32.48 t9ahLiCr.net
ほんとこの1は駄目だなw

765:デフォルトの名無しさん
14/12/07 01:41:10.92 bfkTF4nN.net
lispでC風メソッド呼び出し構文開発したってのをどっかのブログでみたな

766:デフォルトの名無しさん
14/12/07 02:32:50.17 lyVqLM7u.net
リテラルでいろいろ指定できるのは便利だけどな
Clojureだと
{key1 obj1 , key2 obj2}でmap
#{obj1 obj2 obj3} でset
[obj1 obj2 obj3] でvector
'(obj1 obj2 obj3) でlist
地味にsetがありがたかったり(他の言語だとsetのリテラル滅多に無い)

767:デフォルトの名無しさん
14/12/07 12:08:48.39 mrRmmrII.net
>>726
圏論の和書として定評があり再版が望まれているのは
URLリンク(www.amazon.co.jp)
amazon 価格がすべてを物語っている

768:1
14/12/07 17:19:43.84 2ooQYugx.net
いつものようにclojureでconnect4書こうと思ったが、
>>763のことを差し引いても想像以上にモチベーション上がんない。
何のせいだ?
パッと見clojure良さそうに見えるのに。
Prologのときも苦戦したがモチベーションは保てた。

769:デフォルトの名無しさん
14/12/07 18:06:31.44 NlsKlGNA.net
>>768
このスレでは集合論に基づいた言語と関係ない話題はルール違反です。

770:デフォルトの名無しさん
14/12/07 19:50:11.74 npVck0tg.net
>>768
今度は「なぜか分からないけどモチベーションを保てない」かw

>>425>>559>>655-665

771:デフォルトの名無しさん
14/12/08 04:17:29.43 jYPMOE5Q.net
>>768
モチベーションを保てないってことだから続かないと思うけど
続けるならClojureスレに行け

【Lisp】プログラミング言語 Clojure #3【JVM】
スレリンク(tech板)

772:1
14/12/09 23:17:28.28 PZp4J+Rx.net
リアルが忙しくなりそうです。
しばらくこれなくなるかもだが、俺が留守の間おまえらでこのスレを盛り上げてくれよな。
よろしく。

773:デフォルトの名無しさん
14/12/10 21:31:22.32 7P/sQ89x.net
削除依頼していけよ

774:1
14/12/26 19:46:13.23 pkBFPf36.net
仕事納めだよ。
しかし見事にレスがついてないな。
お前らで盛り上げてくれていいのに。

775:片山博文MZ ◆T6xkBnTXz7B0
15/01/03 12:40:55.68 XgnEofgF.net
>>1さんよ、

Coqという言語を使えば、集合論を含む数学の証明や、プログラムの性質や品質保証ができるらしいぞ。
やってみないか?

776:デフォルトの名無しさん
15/01/03 14:07:47.18 MdLSAVWL.net
>>775
>>713-714

777:1
15/01/03 18:31:19.39 y8FDuePZ.net
とりあえず片山さんがCoqで一番成功してると思った例題を教えて
それで判断するわ。

778:片山博文MZ ◆T6xkBnTXz7B0
15/01/03 19:06:58.41 XgnEofgF.net
俺もCoqについては初心者だが、数学、グラフ理論の超難しい問題
「四色問題」の証明がCoqでできたらしい。

779:1
15/01/03 20:02:04.73 y8FDuePZ.net
手続き型言語とかに比べて完結に実装できるってこと?面白そうではある

780:1
15/01/03 20:38:21.69 rEeqS3sH.net
ID違うと思うけど1です。
簡潔に実装できるんじゃなくて、
実装はHaskellとかでやって、その正しさをCoqで保証するの?
よくわからん。

781:1
15/01/03 21:16:03.70 rEeqS3sH.net
Coq単体で動くのか。
prologに近いのか?
ぶっちゃけかなりむずいなこれは。

782:1
15/01/03 22:17:48.00 rEeqS3sH.net
わからんということがわかった。
底なし沼みたいな感じやなこれ。

783:デフォルトの名無しさん
15/01/03 23:44:50.02 Y5c4kVu7.net
今回のクレクレ・ループは終わりかな。

>>425>>559>>655-665

784:1
15/01/04 13:03:03.07 1dxkxQcz.net
片山さんはCoqどれくらい書けるの?
例えばド、モルガンの証明とか書けるの?

785:片山博文MZ ◆T6xkBnTXz7B0
15/01/04 21:15:57.30 izkph8nP.net
>>784
TutorialのPDFをコンビニで2in1pageで両面印刷して研究し始めたとこ。
数学と論理学と英語とプログラミングの知識が要求される地獄山だな。

786:1
15/01/04 21:40:34.76 7jAGFdTv.net
>>785
そのチュートリアルのURLくだしあ。

787:片山博文MZ ◆T6xkBnTXz7B0
15/01/04 21:45:09.09 izkph8nP.net
>>786
「Coq tutorial PDF」で検索

788:デフォルトの名無しさん
15/01/04 21:59:00.42 7jAGFdTv.net
URLリンク(coq.inria.fr)
これ?
結構分量ありますね。

789:1
15/01/06 00:03:50.53 iQ4UNt/k.net
Coqで任意の自然数nに対してn*(n+1)が偶数であることを証明しようとしたがどうしてもできない。
だれかHELP.

790:1
15/01/06 00:34:25.70 iQ4UNt/k.net
定義はこれで。
Theorem t:
forall (n:nat),exists m , (n*(n+1) = 2 * m).

791:デフォルトの名無しさん
15/01/06 05:55:25.49 Gduz5N96.net
偶数+1は奇数
奇数+1は偶数
遇数*奇数も奇数*遇数も遇数
自然数は奇数か偶数かどちらかである

792:1
15/01/06 21:04:14.92 iQ4UNt/k.net
「nが奇数ならn+1は偶数」を証明しようとして詰まってる。

Require Import Even.

Lemma l:
forall (n : nat), odd n -> even (n+1).

intros.

induction n.

simpl.

apply even_S.

これでodd 0とかいうのが出てくるけど、ここからどうしていいかわからない。

793:1
15/01/06 21:10:59.52 iQ4UNt/k.net
「自然数nに対してn*(n+1)が偶数である」
本題のこっちはここまで進んだ。

Require Import Even.

Theorem t:
forall (n:nat), even (n*(n+1)).

intros.

apply even_mult_aux.

794:1
15/01/06 23:17:17.43 iQ4UNt/k.net
Coq難しすぎんよ~
もう寝る。

795:1
15/01/07 19:22:04.95 DdlkDaa+.net
URLリンク(www.iij-ii.co.jp)
このページによるとforall (P : Prop), P \/ ~ Pは証明できなんだそうだ。
forall (n:nat), even (n*(n+1)).も証明できないのかもしれないな。

796:デフォルトの名無しさん
15/01/07 20:14:30.38 zH4wOwdk.net
1に餌を与えないでください。
>>425>>559>>655-665

797:1
15/01/07 21:02:58.84 DdlkDaa+.net
odd 0 -> Falseは証明できたっぽい。
これをどう活用すればいいのかわからない。

Lemma l2:
odd 0 -> False.

apply not_even_and_odd.

apply even_O.

798:デフォルトの名無しさん
15/01/08 15:50:20.90 FouB2F9v.net
S

799:デフォルトの名無しさん
15/01/08 18:29:26.11 qFLJfmjp.net
O

800:デフォルトの名無しさん
15/01/08 19:09:01.13 XNa5H7Wz.net
S

801:1
15/01/08 20:07:08.21 9tH8cNHX.net
ハルヒか?

802:1
15/01/08 22:27:11.24 9tH8cNHX.net
そもそもodd n -> even (S n)って定義そのものなんだよなぁ。

803:1
15/01/11 19:52:52.15 zln55Xsd.net
ギブアップ。
だれか正解しってたら教えて。

804:1
15/01/13 18:35:43.03 7YFvdf+i.net
片山さん答え知ってたら教えて

805:デフォルトの名無しさん
15/01/13 20:23:10.10 ElusS0xD.net
スレリンク(tech板:23番)
> 23 名前:片山博文MZ ◆T6xkBnTXz7B0 [sage]: 2015/01/13(火) 18:53:35.00 ID:gURRjQHf
> 私はお下品

806:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 21:52:38.35 gURRjQHf.net
ヒント。
Require Import Even.
Lemma eSr: forall n:nat, even (1 + n) -> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.

807:1
15/01/13 22:46:33.61 ld5ZWEPI.net
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を偶数と奇数に場合分けする方法がわからんとです。

808:1
15/01/13 23:04:11.48 ld5ZWEPI.net
even(1+n)にeven(1+n) -> odd nをapplyして odd nにならんのか?
よくわからん。

809:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 23:09:34.67 gURRjQHf.net
Lemma oS: forall n:nat, even n -> odd (S n).
intros.
apply odd_S.
apply H.
Qed.

810:1
15/01/13 23:38:41.86 ld5ZWEPI.net
証明済みのLemmaの活用の仕方がわからんです。
applyじゃないの?

811:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 23:39:26.18 gURRjQHf.net
replace (even (S n)) with (odd n).
apply even_or_odd.
もう少しだな。

812:1
15/01/14 00:05:14.20 upPMt0VH.net
A=Bを示したかったらA->BかつB->Aで方針あってますか?

813:1
15/01/14 00:09:20.78 upPMt0VH.net
もう寝ます。
また明日よろしくお願いします。

814:片山博文MZ ◆T6xkBnTXz7B0
15/01/14 19:03:17.31 lWtQJ7uI.net
聞きたいことがあれば、俺の掲示板に来いよ。待ってるぜ。

815:片山博文MZ ◆T6xkBnTXz7B0
15/01/15 14:58:59.94 OiYOltU9.net
URLリンク(katahiromz.bbs.fc2.com)

816:デフォルトの名無しさん
15/01/15 18:04:49.36 UYCK2hGt.net
>>814-815
1がそっちに行ってくれればいいけど。
1はCoqとか本当はどうでもよくて、このスレに書くこと自体が目的になってるだろうから・・・

817:デフォルトの名無しさん
15/01/15 20:46:59.13 QgJ4DA/V.net
>>816
雑談はこちらの412に書いてるな。
戻ってくるなよ >1

818:1
15/01/15 21:04:35.89 RCkerH2f.net
お前らこのスレが伸びちゃ困る理由でもあるのかw

819:デフォルトの名無しさん
15/01/15 22:49:41.86 5ppshwSd.net
>>818
1が「集合論に基づいた言語を作る」話をしないからな。
>>425>>559>>655-665

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

820:1
15/01/15 23:03:37.94 RCkerH2f.net
このスレはお前らで盛り上げてくれてもかまわないんだぜ?

821:デフォルトの名無しさん
15/01/16 00:08:32.30 q80wbXpz.net
このスレ見てるの結構楽しい(煽りとかではなくいろんな話が出てくるし)から盛り上がって欲しい

822:1
15/01/16 00:10:36.55 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
15/01/16 01:05:01.69 IPI8U3lP.net
>>822
なかなかやるじゃん。

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

片山QZの定理
URLリンク(katahiromz.web.fc2.com)

824:1
15/01/16 18:38:49.28 tbQRRWp6.net
MZとかQZとかって何なの?
別にいいんだけど。

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

825:片山博文MZ ◆T6xkBnTXz7B0
15/01/16 18:52:49.05 IPI8U3lP.net
QZというのはC/C++宿題スレに生息している人だよ。

そうだな。2n=n+nの証明なんかどうかな? 楽勝?

826:1
15/01/16 19:09:16.59 tbQRRWp6.net
掛け算の定義がどこにあるのかわからん。

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

827:片山博文MZ ◆T6xkBnTXz7B0
15/01/16 22:32:01.39 IPI8U3lP.net
>>826
英語では、掛け算がmultiplicationで、自然数がnatural numbersだろ?
それを略すればmul,natになるだろ?
SearchAbout mul.
SearchAbout nat.
で検索できるから。

828:1
15/01/16 23:47:30.80 tbQRRWp6.net
>>827
結構むずかしい。
仮にできたとしても時間かかると思う。

829:1
15/01/17 00:13:16.15 e9PIZEl5.net
ぶっちゃけCoqやってると無限に時間を吸われる可能性がある。
早めに身を引いた方がよさそうかな~とも思う。

830:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 01:27:28.08 PPUSm5YO.net
数学に基づいた言語としてCoqは最適の例かと思われたが、御気に召さないとはこれ如何に。
では、そなたはどのような言語が希望か申し上げてみよ。

831:1
15/01/17 02:12:55.60 e9PIZEl5.net
いや~確かにCoq面白いんだけど。
勉強するのに時間かかり過ぎるっていうか
もうちょっと市民権を得て入門書とか充実してからの方がいいかな~と。

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

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

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

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

832:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 02:59:53.32 PPUSm5YO.net
麿は、この素晴らしきCoqを使えば、不具合のないソフトウェアが作れると見ては、
これをマスターすれば世界征服も夢ではないと、そのような所存でおじゃるよ。

833:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 03:31:41.14 PPUSm5YO.net
Coqと人工知能を組み合わせたら……、金融取引に活かせば……とか楽しい妄想が広がるでおじゃる。

834:1
15/01/18 22:30:12.77 Pnbu8M/I.net
人工知能といえばdeep learningとかいうのが流行らしいんだが。


次ページ
最新レス表示
レスジャンプ
類似スレ一覧
スレッドの検索
話題のニュース
おまかせリスト
オプション
しおりを挟む
スレッドに書込
スレッドの一覧
暇つぶし2ch