次世代言語11[Rust Swift TypeScript Dart]

1 名前：デフォルトの名無しさん [2018/06/03(日) 23:53:27.92 ID:vrBh4O6u.net] スレタイ以外の言語もok 前スレ 次世代言語10[Rust Swift TypeScript Dart] https://mevius.5ch.net/test/read.cgi/tech/1524607347/ 522 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:22:09.07 ID:iWNJr2Uz.net] 「新しいものを導入しよう」とか脳死でわめくガキに現場しっちゃかめっちゃかにされる経験がないのか それとも逆に現場ひっかきまわす側のガキなのか 次世代っていうのは目新しさで決めるもんじゃないだろ 523 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:22:47.73 ID:SIx1eJMh.net] >>514 現場知ってるならJava8なんて出てこない あ、奴隷かごめんね 524 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:24:24.84 ID:aJjY8hhI.net] Dが目新しいってマジ？ 525 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:28:42.12 ID:iWNJr2Uz.net] >>516 5、6年後くらいのリプレイス時にJava8導入するかもしれないから互換性の下調べしてる段階な お前のいう「現場知って」る奴ならどんな言語出すんだ？ まさかことりんとか言わんよな？ 526 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:32:58.06 ID:8e4AMBWv.net] このスレに上がってるような言語を実践投入する時はそら1990年代にJavaを投入した時のように慎重にいかないといかんでしょ 脳死での実践投入なんて発想が最初に出てくるとかガイジか。いや、ドカタだからそういう常識が欠けているのか。ごめんね？ 527 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:33:35.47 ID:yCU9+KnB.net] 商用開発的に色んな側面考慮してJava8選択するのは特におかしいとは思わないけど 次世代呼びは流石に無茶やって 528 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:35:35.09 ID:iWNJr2Uz.net] >>519 おまえさんは違うと思うが、 実際いるんだよ脳死実践投入主張するガキが…… 529 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:38:30.24 ID:iWNJr2Uz.net] >>520 Java8が次世代じゃないとか言い出すとは思わんかった Java8以上に新しい言語は次世代通り越して未完成言語って言ってもいいわ 530 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:44:30.75 ID:8dIO3AYC.net] >>513 使ってる案件あります？ TypeScriptはES2015+型って考えでとりあえずは使えるから、学習コストは低い。 this問題はアロー関数でも使っとけばいい。 531 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:46:16.06 ID:8dIO3AYC.net] >>502 人材がいないのにどうやって集めろっていうの？ 532 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 16:50:08.16 ID:8dIO3AYC.net] >>502 別に新しい技術で人材不足を解消しようって話はしてないよ。 間違った行間読みはやめろ。 純粋に案件を始めるにあたって、 言語を特殊なものにすると、人材が集めづらいだろって話。 TypeScriptというメジャー寄りの言語ですら、専門以外エンジニアになりがちって話。 ちなみにTypeScriptは学習コストは低いほうだ。 533 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 17:00:54.21 ID:TG/aPZPS.net] サポート切れるのに今からJava8を選ぶって逆に脳死過ぎだわ The老害にも程がある 534 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 17:03:31.92 ID:4b7uuLRW.net] >>514 現場ﾜﾛﾀ おまえに必要なのはJavaでもTypeScriptでもない Excel方眼紙だ！ 535 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 17:12:42.29 ID:u2X2MJCJ.net] JVM系言語は全滅と思っていいのかね 536 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 17:43:45.20 ID:erltHdM+.net] >>524 知るか。派遣でもなんでも雇えば良いだろ？ >>525 > 間違った行間読みはやめろ。 すまんな…でも、あの文脈じゃそういう風に受け取られても仕方ないと思うけど… > 言語を特殊なものにすると、人材が集めづらいだろって話。 集めづらいよ。だから慎重に検討する必要はあるし、手放しに喜んで良い機能じゃない ただ時々「慎重に検討する」を曲解して「結局、絶対に採用されない」と 新しい技術そのものを否定しようとするヤツが居るんで それは違うだろ？将来に備えて勉強しておく必要はあるだろ？ 自分が理解できなかったのを正当化するための言い訳だろ？って言いたい あと、慎重に検討した結果、採用したとして、それでも失敗した場合は それは経験として受け入れるべきであって失敗として否定するべきではない ある程度のリスクは受け入れないと、失敗はしなかったとしても成功もしない どの程度のリスクを許容するかのバランスの問題であって、 全くリスクを受け入れようとしない企業は所詮その程度の企業だってこと 537 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 17:53:45.44 ID:iWNJr2Uz.net] >>527 Excelも年々進化してるんだがお前は知らんのか？ バカにしてるやつはその程度か 538 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 17:55:57.69 ID:OuCJaAt5.net] 図星で草 539 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 18:10:25.08 ID:7oGqe5zS.net] おじいちゃんにはkotlinは難しすぎるらしい 540 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 18:16:25.72 ID:SIx1eJMh.net] >>518 5、6年後にJava8ｗｗｗ 541 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 18:43:07.15 ID:iWNJr2Uz.net] >>533 なんかおかしいか？枯らす期間としては短い方だろ 542 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 18:54:54.59 ID:a73jVlJK.net] 寿司職人が5、6年修行しているようなものか 半年でできらぁって誰かが言い出したとしてお前らはそいつを倒せるのか？ 543 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 19:15:51.85 ID:SIx1eJMh.net] >>534 何がおかしいのかわからないようならこの業界やめた方がいい 544 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 19:18:30.51 ID:510xBBBe.net] Java8のどこらへんが次世代なのかは言わんのな 545 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 19:26:09.30 ID:iWNJr2Uz.net] >>535 倒すだの勝つだの物騒な話してねえから 安定したプログラムを工数圧縮して作るのが目的だから 546 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 20:20:10.90 ID:En9MtaF9.net] >>518 Java8 のサポート期間いつまでか知ってるかい？ 547 名前：デフォルトの名無しさん [2018/06/17(日) 20:25:05.46 ID:p2Sm4Lro.net] たぶ今頃サンに問い合わせてるんだろな 548 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 20:38:25.12 ID:SLSvvYl3.net] 導入したい技術は、きちんと上司に根回しして 承認印を頂くこと 549 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 20:43:39.42 ID:dJUJdMR3.net] 上司がバカな可能性も十分あるからなんとも言えん。 しかし、同じくらいの割合でバカな新人が新しいクソツールをねじ込むこともあるからな。 一般に表面だけ見て判断はできんわ。 550 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 20:50:01.61 ID:wbEMQisX.net] 五年後からJava8とか地獄のような現場もあったもんだな 現場を知らなかったわ 551 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 20:55:06.44 ID:wY+r/3B/.net] アップデートがあるうちはまだまだ未完成 LTSが終了したところで真の安定板になるのですよ… 552 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 21:26:03.64 ID:u2X2MJCJ.net] そろそろ次世代の話がしたい 553 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 21:27:10.33 ID:wbEMQisX.net] 現場知ってる人にASTの話題流されたからな 554 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 21:34:27.48 ID:Nk/Dtbgv.net] Java8は流石にネタだと信じたい ネタとしては面白かったけど 555 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 21:44:52.52 ID:Zsovn15r.net] 面白かった次スレから入れるか？ｗ 556 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 22:04:53.41 ID:SLSvvYl3.net] やれやれ・・・（肩をすくめ、冗談だろ？と失笑しながら、イケメンを少し崩した変顔でつぶやく僕） 557 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 22:19:46.98 ID:IxLGC6rA.net] 昔クソツールと言ってgradleを拒否した爺さんが弊社にいた 蓋を開けてみると新しいからダメっていうか爺さんがわからないからごねてただけだった 爺さん今はKotlinを猛烈に攻撃してる こういうのって沢山あるんだろうな 558 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 22:32:18.24 ID:EBuoSE6p.net] サポート終わったものは社内のセキュリティ監査で引っかかるから使えんけどなあ 559 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 22:36:34.77 ID:dJUJdMR3.net] >>550 逆もまた然り。 rails 無理やり使わせてメンテせず逃げたバカを何人も知っとるわ。 560 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 22:59:16.75 ID:iFYzb9cl.net] ドカタ言語としてはJava SE 1.4くらいがちょうどよかった。あれのLTSがあったらなぁ。 561 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 23:00:14.53 ID:9aKhKpN8.net] C#やりたいなあ 562 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 23:06:55.31 ID:SLSvvYl3.net] railsはさすがにゴミですわ ド型にすらなれないゴミ 563 名前：デフォルトの名無しさん [2018/06/17(日) 23:21:54.59 ID:p2Sm4Lro.net] グレードルもクソだと思うけどそもそもjavaがクソなのでツールを責めるのは酷だすな コトリンは救いようがない滅せよ 564 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 23:28:49.24 ID:dJUJdMR3.net] 言語もそうだがクソなものを勧めてくる奴の特徴は おそろしくモジュラリティーの低いものばっかり勧めてくるってところだ。 565 名前：デフォルトの名無しさん mailto:sage [2018/06/17(日) 23:47:42.67 ID:Zsovn15r.net] その発言！η変換すると「クソなものはモジュラリティが低い」になるぜ！ 566 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 00:41:09.48 ID:szLLB6p9.net] >>556 やっぱりそうなったか… 場当たり的な甘さがこれほど早く破綻をまねく分野もない 567 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 00:44:39.69 ID:szLLB6p9.net] >>559 kotlinなにがだめだったん？ 568 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 00:44:54.86 ID:szLLB6p9.net] >>556 569 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 00:56:40.78 ID:5zfP7m4z.net] gradleがクソはまあわかるがantよりはマシ 爺さんがごねなきゃ最低のクソから並みのクソぐらいには昇格できたかもしれない 新技術拒否爺さんは業務効率化を阻む害悪でしかない 570 名前： mailto:sage [2018/06/18(月) 01:07:58.13 ID:OiAJbwiy.net] >>555 今から rails に取り組もうと思っていたのですが…（?然） 571 名前：デフォルトの名無しさん [2018/06/18(月) 01:49:33.50 ID:2+ok0PtZ.net] 気にすんな。世の中には自分の能力が足りなくて理解できないものをクソだということにして 自分の心を安定させようとするやつが居るってだけのことだから。そういうやつは何千年も 前から居る。ほとんど人間という動物の習性だと思っていい。誰でもそういう状態にハマる 可能性がある。ハマってる最中はそいつは他をクソ呼ばわりするだけで新たな事は何も 学習しなくなるので馬鹿な状態が維持されて発展しない。 572 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 07:01:11.25 ID:Jei0+sA2.net] >>563 いい加減に板を荒らすのやめろよ 特にここ最近はRubyスレを荒らしまくって何考えてんだ？ 573 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 07:13:46.91 ID:wJzzPYpc.net] >>564 歴史に何も学ばないやつに発展はない。 https://anond.hatelabo.jp/20171129214218 565はこの種のバカなことを引き起こしといてトンズラするタイプだな。 だいたいこのタイプは仕様が満たされるものだと過信してるタイプで 機能の堅牢性なんてまともにチェックしてない。 574 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 07:25:45.84 ID:OPxRI0Cf.net] 歴史を学習した人間より科学を学習した自動運転の方が安全というのが シンギュラリティの思想だよな 575 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 08:03:14.74 ID:GT4ypnkz.net] >>564 それを「固定された思考態度」という。 576 名前：デフォルトの名無しさん [2018/06/18(月) 08:19:55.49 ID:AHTeguQN.net] どっちも危険な盲信になりえる >>564 みたいに一方的なのは危険 577 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 10:03:33.26 ID:1wi3jEJk.net] 「新しいものをバカみたいに導入しようとする奴は危険」ってのはまあその通りなんだが 上の「5年後にJava8を導入おじさん」も同じくらい危険人物な訳で 結局突き詰めてメリデメリをジャッジできる思考力ないだけのバカは開発を地獄にするってのは変わらんよね 578 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 11:21:38.28 ID:cgeQ1bE7.net] プロコンという語を覚えると便利だよ>メリデメリ 英語のプレゼンでprosとかconsとか見たことあるでしょ？まあ英語というかラテン語なんだけど。 579 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 11:40:21.90 ID:OPxRI0Cf.net] デメリット、コスト、人月の見積もり 見積もりを妄信するのも危険と言われる 580 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 13:11:53.12 ID:byOf5Soa.net] >>449 ＞>>448 ＞なんと！ ＞日本語審査会で審議しないといけないな。 言い忘れたがこの混同は英語でもある というか放射能漏れは leakage of radioactivity の直訳 581 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 14:05:58.53 ID:7nYEmGe5.net] そもそも次世代言語が次世代なうちは個人の趣味プロぐらいにしか使わんだろ 582 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 14:33:09.83 ID:sQTrKk9Y.net] HaskellやElixirを実業務で使ってるところも 実在するわけだよな恐ろしい 583 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 14:45:17.24 ID:UoKY4/G0.net] そのへんはむしろ枯れてるし実際ある 584 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 14:48:34.03 ID:soq2obRK.net] まあHakellに関してはもう次世代というよりLispと似たようなポジションだということで 585 名前：デフォルトの名無しさん [2018/06/18(月) 15:30:15.87 ID:soq2obRK.net] ところで、またATS2に話を戻すんだけど、 日本語訳もあったしチュートリアルやってみてるんだけど ↓の再帰関数の停止性検査とやらで躓いている ttp://jats-ug.metasepi.org/doc/ATS2/INT2PROGINATS/x2485.html 特に fun isevn{n: nat} .<2*n>. (n: int n): bool = if n = 0 then true else isodd (n-1) and isodd{n: nat} .<2*n+1>. (n: int n): bool = not(isevn(n)) が何故.<2 * n>.と.<2 * n + 1>になるか理解できん… .<n>.と.<n + 1>.で大丈夫だと思ったんだが… たぶんまだ、停止性メトリクスとやらが正しく理解できていないんだろうな… 誰か詳しく解説してくれないか？ 586 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 15:31:22.53 ID:/sFO+jYl.net] >>575 ドワンゴ（失笑）とかか？wwww 587 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 15:37:03.09 ID:/sFO+jYl.net] ドワンゴが使ってると公言した言語を使ってる会社はドワンゴレベル 気を付けろwwwww 588 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 16:10:43.68 ID:soq2obRK.net] ドワンゴってScala以外にもSwift, Kotlin(スマホアプリ)やReact(Typescript)やRustとかも使ってるからな… 開発事例は聞いたことないけどGoの勉強会とかもやってるし… その基準だと、このスレでよく話題に挙がる言語はほとんど全てドワンゴレベルだな ドワンゴレベルじゃない次世代言語はDartくらいか？www 589 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 16:24:24.97 ID:NEyGx0zg.net] ドワンゴには、C++ の標準化委員の江添亮もいるし、Rust, Elixir, HDL もやってる。 クックパッドには、RubyVM を作った、笹田耕一もいる 基本は、Ruby。 Gradle で使うGroovy も、Ruby そっくり。 Elixir もそう。 jQuery のメソッドチェーンも、Ruby っぽい 無料のRails チュートリアルをやれば、すべてのフレームワークがわかる 590 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 16:24:43.92 ID:yVgz9/Zm.net] 言語と品質には何の関係もないのを 日々実証し続けているドワンゴさん 591 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 16:29:30.09 ID:pZ1JIWjn.net] まだRubyのチュートリアルの話してんの？ Rubyっぽい、って、第一言語がRubyだからそう見えるだけだろ。 592 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 16:40:07.48 ID:OPxRI0Cf.net] フリーソフトがあるから品質と価格が無関係 593 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 17:22:50.97 ID:qMNnTEHn.net] ドワンゴってエンジニアだけ見ると技術力高そうなのに なんで成果が全部ゴミなんだろうな 594 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 17:37:58.73 ID:NEyGx0zg.net] YouTube, AbemaTV は、広告 ニコ生は、有料 Showroom は、寄付 ビジネスモデルが異なるから、 1つのチャネルの視聴者数が1万を超えると、追い出す 乃木坂みたいに、数万人も見ると、追い出す。 広告が無いから、1万人以上が無料で見ると、電気代が払えず、赤字になる 595 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 18:02:04.30 ID:EvkbZGBx.net] >>578 isevn.<n>.とisodd.<n+1>.だと isevn 3 のメトリックは.<n>. = .<3>. そこから呼ばれるisodd 2 のメトリックも.<n + 1> = .<3>. 減ってねえ！エラー！ってことじゃね 想像だけで試してないので違ってたらすまん 596 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 18:04:53.53 ID:xdRdwSco.net] >>578 とある関数呼び出しの定義内に表れる再帰的呼び出しの 停止性マトリクスが、大元の関数呼び出しの停止性マトリクスから辞書順で下降していくことから停止性を担保しようというのが停止性マトリクスの意味。 そして停止性マトリクスの記述に表れる n は issven や isodd の引数そのものだということに注意 iseven、isodd の停止性マトリクスがそれぞれ n、n+1 だと、 iseven n の停止性マトリクス→n iseven n の定義に出てくる isodd (n-1) の停止性マトリクス→n-1+1=n 減っていないから停止性が担保されない(NG)。 説明にあるように <n, 0> と <n,1> ならば、 iseven n の停止性マトリクス→<n,0> iseven n の定義に出てくる isodd (n-1) の停止性マトリクス→<n-1,1> (下降している！OK) isodd も同様に isodd n の停止性マトリクス→<n,1> isodd n の定義に出てくる iseven (n) の停止性マトリクス→<n,1> (下降している！OK) そして<n,0>, <n,1> の代わりに n*2, n*2+1 を使っている(この代用が可能なことはわかるよね)。 597 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 18:08:28.85 ID:xdRdwSco.net] >>589 ＞停止性マトリクスが、大元の関数呼び出しの停止性マトリクスから辞書順で下降していくことから停止性を担保しようというのが停止性マトリクスの意味。 この説明「下降していく」だと本当に再起をどんどん 実行していくみたいで間違ってるか。 とある関数呼び出しの停止性マトリクスよりも、 その関数の定義に表れる全ての再帰的呼び出しの停止性マトリクスのほうが辞書順で小さい、 というべきか。 598 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 18:09:50.53 ID:xdRdwSco.net] >>589 ＞isodd も同様に ＞isodd n の停止性マトリクス→<n,1> ＞isodd n の定義に出てくる iseven (n) の停止性マトリクス→<n,1> (下降している！OK) 最後の行は isodd n の定義に出てくる iseven (n) の停止性マトリクス→<n,0> (下降している！OK) の間違いでした 599 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 18:32:21.74 ID:NEyGx0zg.net] 偶数は、2*n 奇数は、2*n+1 600 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 18:34:45.57 ID:EvkbZGBx.net] >>592 理解してないだろw 601 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 18:51:32.37 ID:OPxRI0Cf.net] 安全装置のたぐいは損失を防ぐばかりで利益は全然ない 利益がないから理解できない人が続出 602 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 18:58:41.11 ID:soq2obRK.net] >>589 ありがとう 冷静に計算していったら、確かにnとn+1じゃ減ってないからダメで 2*nと2*n+1だときちんと減ってるからOKってところまでは理解できた でも、一体何を考えて<n,0>と<n,1>のタプル？のメトリクスが出てきたか全然分からない… > そして<n,0>, <n,1> の代わりに n*2, n*2+1 を使っている(この代用が可能なことはわかるよね)。 すまない。俺はバカなんだ。分からないんで教えて下さい。 自分でも自分がどこまで分かっているのかさえよく分かっていないんだが、 たぶん、停止性メトリクスがきちんと減っているかどうかを計算する方法までは理解できたが、 きちんと減っている停止性メトリクスを導き出す方法が分かってないんだと思う 603 名前：ﾌ名無しさん mailto:sage [2018/06/18(月) 19:23:14.64 ID:xdRdwSco.net] >>595 ＞すまない。俺はバカなんだ。分からないんで教えて下さい。 辞書順を保ったまま <n, 0>, <n,1> をそれぞれ 2*n, 2*n+1 で置き換えられる 3*nとか4nでもいいけど2つしかないから2nで十分 例 fun f {n:nat} .<3*n>. (n: int n) : bool = if n = 0 then true else g (n-1) and g {n:nat} .<3*n+2>. (n: int n) : bool = not (h (n)) and h {n:nat} .<3*n+1>. (n: int n) : bool = not (f (n)) 604 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 19:24:20.04 ID:EvkbZGBx.net] >>595 引数のnと、isoddとisevnの2つの関数の区別(+0, +1)を位取り(*2)して足してるだけじゃないかな…… 605 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 19:33:04.83 ID:vrc1WpPf.net] >>581 全部そうだよ やっぱりJavaやC、Pythonが最終的に一番良いってことだな 新しいものに飛び付いてるとドワンゴになるぞ 606 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 19:52:57.33 ID:wJzzPYpc.net] ドワンゴはc++みたいなもんだな。 とりあえず新言語(新機能)の実験台になってもらえるっていう。 607 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 20:40:04.20 ID:bcKP+A2z.net] >>599 つまりドワンゴがスレタイ言語は ほぼ使えないと証明してくれてるってことだな 608 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 20:46:12.17 ID:7nYEmGe5.net] ドワンゴは本当のC++プログラマーも募集してるしな 609 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 21:40:32.50 ID:poCVJCAd.net] やきそば焼かせてるようなクズ会社にいくのか？ 610 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 21:49:26.33 ID:c5Ieze8t.net] bio100%の戀塚もいるんだよな いかんせん上がアホだから 611 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 21:55:35.52 ID:soq2obRK.net] >>596 辞書順を保ったまま置き換えられるってのが何をしてるのかイマイチよく分からんが とりあえず、2つの関数で相互再帰なら2n、3つなら3nといった感じ……なのか？ うーん…まだ勉強し始めたばかりだし、やってればそのうち分かるようになるかぁ… あざっす。 612 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 22:18:33.96 ID:ejyTxCd5.net] >>604 いやここで堪えて理解しておくべき。 引数から算出できて、再帰で減るものを何か考えてそれを停止性マトリクスとする。 値そのものじゃなく大小関係だけが大事だから、 m が 0 と 1 のどちらかしかなければ <n, m> の代わりに n*2+m で ok ってこと 例 <5,0> は <4,1> より大 ⇔ 5*2+0 は 4*2+1 より大 613 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 22:30:23.80 ID:ejyTxCd5.net] ちなみに辞書順というのは停止性メトリクスのタプルについて、 先頭の要素同士を比較、等しければ次の要素同士を比較、また等しければそのまた次の以下略… という風に比較したときの順序関係 614 名前：デフォルトの名無しさん mailto:sage [2018/06/18(月) 22:47:52.93 ID:ejyTxCd5.net] 上で散々マトリクスと誤記しているメトリクスはこの場合「(停まるまでの)距離」という意味 615 名前：デフォルトの名無しさん [2018/06/18(月) 23:09:05.63 ID:soq2obRK.net] >>605 なるほど。(n, 0)と 616 名前：(n, 1)が2nと2n+1に変換できることまでは分かった。ありがたい。 でも、そもそもの話として(n, 0)と(n, 1)っていうのが 一体何を考えて導き出されたのかが分からないんだよ… チュートリアルに「isevn と isodd に (n, 0) と (n, 1) のメトリクスを与えれば、 これら2つの関数の停止性もまた検査できることは明白です。」って 書いてあるんだけど、俺にとっては全然明白じゃない… 何をどう考えたら(n, 0)と(n, 1)のメトリクスを与えようと思うんだ…？ 現状、分かっているのは2nと2n+1ならメトリクスが減っているからOKってところと (n, 0)と(n, 1)のメトリクスが2nと2n+1に変換できるってところまで… 一番肝心な部分が理解できていない気がする… [] [ここ壊れてます] 617 名前：デフォルトの名無しさん [2018/06/18(月) 23:17:38.17 ID:Tp0/3gfg.net] なんの話か分からないけどこういう奴らが使ってる技術は使いたくない 618 名前：デフォルトの名無しさん mailto:sage [2018/06/19(火) 00:28:07.36 ID:2myyjakz.net] ATSは依存型言語の中でも奇抜な方だと思うよ Coqとソフトウェアの基礎の方が易しいと思う 619 名前：デフォルトの名無しさん mailto:sage [2018/06/19(火) 01:44:59.48 ID:menX4d1R.net] CoqとAgdaは敬遠してるんだよね… あの二つはプログラミング言語じゃなくて証明支援器だって聞いてるから… オレは別にPCに証明問題を解くのを手伝ってもらいたいんじゃなくて、 従来の型システムを発展させた依存型とかを使ったより安全な プログラミングを行うの方法が知りたいんだよって思って… けど、学ぶ順番としてはCoqが先のほうが良かったのかな？ でも、Coqだとどうにもモチベーションが… あと、ついでに線形型も学びたかった…… Rustの所有権・借用・ライフタイムはほぼ理解できてるんでそれほど難しくはないだろうと… まず、依存型で躓いてるんで線形型までたどり着いていない… んー……一度に色々やろうとし過ぎか…(´・ω・｀) 620 名前：デフォルトの名無しさん mailto:sage [2018/06/19(火) 02:53:39.62 ID:8GZLihdn.net] Idris とかはどうなのよ 621 名前：デフォルトの名無しさん mailto:sage [2018/06/19(火) 04:24:16.98 ID:thfWBPV2.net] >>608 この場合呼び出しのたびに変化するものが、引数のnと「どちらの関数を呼ぶか」という 2つしかないんだから、呼び出しのたびに減る式を作ろうとしたらこれを組み合わせるしかない 後はパズルだろ 622 名前：デフォルトの名無しさん [2018/06/19(火) 07:30:15.96 ID:3/FXNCrL.net] 全てのｎについて(n, 1)＞(n, 0)と2n+1＞２ｎは同値だから当たり前だろ。

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef