関数型言語ML (SML, OCaml, etc.), Part 6

1 名前：デフォルトの名無しさん mailto:sage [2009/06/15(月) 07:15:21 .net] 関数型言語MLについて語るスレッドです。 MLは、確固とした理論的背景を持つ言語でありながら、 現実的なソフトの開発にも使用できる実用性を備えた言語です。 また、プログラミングの初心者が最初に学習する言語としても優れています。 総本山 Standard ML www.smlnj.org/ Objective Caml caml.inria.fr/ocaml/ 前スレ 関数型言語ML(SML, OCaml, etc.), Part 5 pc12.2ch.net/test/read.cgi/tech/1186292994/ 919 名前：デフォルトの名無しさん mailto:sage [2015/02/20(金) 10:31:17.89 ID:N6pKHonh.net] じゃあ俺は2 920 名前：デフォルトの名無しさん mailto:sage [2015/02/20(金) 10:55:47.88 ID:sOgXDRpH.net] 宿題は自力でやれw 921 名前：デフォルトの名無しさん mailto:sage [2015/02/21(土) 00:55:59.35 ID:KgB/c0aN.net] >>906 Standard ML のレコード型は構造的部分型関係を持たないよ 構造的部分型関係を持つレコード型に類する型を持つのは OCaml や Java いわゆるオブジェクト指向におけるクラスとそれらの間の継承関係のこと また「多相レコード型」という用語の意味が「パラメタ型多相なレコード型」 であるならば、Standard ML は多相レコード型を持つことになる ここでパラメタ型多相は、Java だとジェネリクス(総称型)と呼ばれている 結論として、Standard ML(とその処理系 SML/NL および SML#)は１と３を満たす 次にファーストクラスについて、>>902 のコードにおける関数 get_x の定義だけど、 　「フィールドとはレコード値からフィールド値への写像(関数)である」 という関係に気付けば、その定義は以下のように簡潔になる 　　# val get_x = #X; 　　val get_x = fn : ['a#{X: 'b}, 'b. 'a -> 'b]　　(* SML/# *) つまりフィールド #X は(val宣言で)識別子に束縛したり、他の関数へ適用したり。 ある関数の評価結果として返すことができる こうした数値や文字列といった値と同等に扱える性質を指してファーストクラスと呼ぶ さらに上記の例は SML# だけど、SML/NJ も型システムが単純たから型推論に失敗するだけで、 データ型を明示的に宣言すれば関数 get_x を定義できる 　　- val get_x = #X : {X: real, Y: 'a} -> real; 　　val get_x = fn : {X:real, Y:'a} -> real　　　(* SML/NJ *) 型システムの制約とファーストクラスという性質をごっちゃにすべきではない まとめると、Standard ML(とそのすべての処理系)のフィールドはファーストクラスである 922 名前：デフォルトの名無しさん mailto:sage [2015/02/21(土) 01:03:27.14 ID:KaIHMFIz.net] > 　　- val get_x = #X : {X: real, Y: 'a} -> real; でもこの get_x って、>>902 の point_3d には使えないよね。 923 名前：デフォルトの名無しさん mailto:sage [2015/02/21(土) 01:45:43.43 ID:KgB/c0aN.net] うん、使えない それが >>910 で書いた(Standard ML言語仕様における)「型システム」の制約だね その制約を無くした SML# が特異なだけで、SML/NJ 以外の大半の SML 処理系に同じ制約がある 924 名前：デフォルトの名無しさん [2015/02/21(土) 06:39:28.04 ID:QYKbOsyjA] SML＃はstructual subtype関係　もつんじゃないの？↑のリンク先見る限りさ {l1:a, l2:b} < {l1:a} みたいに扱われないの？ javaの部分型関係は明示的にクラス名に順序関係付けただけのものだけじゃないの？ フィールドをファーストクラスとして扱えるような技があるのはうえの説明で理解した。Thanks. 思ってたより使えるなsml。 一方で、フィールドリテラル自体を、関数経由でなく、ファーストクラスとしてあつかう必要がある/そっちのほうが好ましい かもしれない 上のリンク先にある論文見るかぎり（例えば↓）そういういみでのファーストクラスフィールドは現状は扱ってないと書いてある。 SML# in Industry: A Practical ERP System Developmentn, # val get_x = #X; のXに実行時中に得られる文字列の値を使いたい String str = "myfld"; Rec rec = {str:"yaaa"}; みたいにさ。 うーんsmlでかくか、sml#つかうか、それともJava,Scala,でかくかまような。 型推論は必要ないかもしれないし、sml#ってどこまでメンテされるのか解らないし、SML/NJがいいかな、、しかし>>911がきになるな。 scalaのオブジェクトでレコードをシミュレートするか、、 ファーストクラスのフィールドを持つ、 レコードで構造的な部分型関係をもっているようなのがほしい。 925 名前：デフォルトの名無しさん [2015/02/21(土) 06:49:52.82 ID:QYKbOsyjA] というかここMLのすれだったのか、関数型言語全般かと思った。 926 名前：デフォルトの名無しさん mailto:sage [2015/02/21(土) 20:03:59.94 ID:KgB/c0aN.net] >>910 >Standard ML のレコード型は構造的部分型関係を持たないよ >構造的部分型関係を持つレコード型に類する型を持つのは OCaml や Java >いわゆるオブジェクト指向におけるクラスとそれらの間の継承関係のこと 自己レスだけど、この段落は間違いが含まれていたので訂正する まず： >Standard ML のレコード型は構造的部分型関係を持たないよ この文章は正しいけど、SML# は「構造的」部分型関係に類する型を持つ だから >>902 の関数 get_x は point_2d とpoint_3d のどちらにも適用できる(>>911) そして SML# だと、point_2d と point_3d のそれぞれの型について、 {X: real, Y:real} >= {X: real, Y:real, Z: real} という部分型関係を持ち、 ここで 関係 a >= b は「a の部分型が b である」ことを意味する 次に： >構造的部分型関係を持つレコード型に類する型を持つのは OCaml や Java >いわゆるオブジェクト指向におけるクラスとそれらの間の継承関係のこと この文章は完全な間違いで、正しくは 「「非構造的」部分型関係を持つレコード型に類する型を持つのは OCaml や Java (...後略)」になる たとえば(架空言語で)二次元座標上の点として 抽象クラス {} を定義し、その具象クラスとして {X軸: real, Y軸: real} および(原点からの相対的な) {角度: real, 距離: real} を定義できる ここで、２つの具象クラスのフィールド構成(=内部的構造)は全く異なるけれど、 {} >= {X軸: real, Y軸: real} および {} >= {角度: real, 距離: real} という部分型関係を持つ 927 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/03/06(金) 00:20:10.28 ID:Utx2vhNJ.net] MLで株取引してるヤツおる？ 928 名前：デフォルトの名無しさん mailto:sage [2015/03/06(金) 19:18:02.97 ID:z8rf25M9.net] >>916 https://www.janestreet.com/ 929 名前：デフォルトの名無しさん mailto:sage [2015/04/11(土) 09:23:04.09 ID:4MGH5loU.net] 『関数型プログラミングに目覚めた! IQ145の女子高校生の先輩から受けた特訓5日間』 www.amazon.co.jp/dp/4798043761/ なんか面白そう。 ベストセラー１位だし。 930 名前：デフォルトの名無しさん mailto:sage [2015/04/11(土) 11:09:33.39 ID:6e+Pm3/z.net] 著者名みてどん引き 931 名前：デフォルトの名無しさん mailto:sage [2015/04/11(土) 14:52:19.95 ID:kM0sKeAC.net] >>918 まーたハゲの人バカやってるのか 932 名前：デフォルトの名無しさん mailto:sage [2015/04/30(木) 22:13:28.21 ID:CyAc4DaC.net] これあわせで、qiitaで何ヶ月か前に宣伝始めたんだよな。 今回のMSの開発者向けイベントで、マルチプラットフォームアピールしてたから、F#にもチャンスが増えるかも。 933 名前：デフォルトの名無しさん mailto:sage [2015/06/21(日) 14:35:56.40 ID:jZdgW1bu.net] ML系でマルチスレッドプログラミングってどうやるの？ できれば、プリエンプティブで。 ノンプリなら、バインディングさえ準備できればpthreadとか使うだけで出来る? あと、マルチコアで動く処理系ってどんなのがありますか？ 934 名前：デフォルトの名無しさん [2015/06/21(日) 15:56:19.44 ID:h+2IwqsQ.net] ノンプリエンプティブな並行のフレームワークとしてはConcurrent ML、 マルチコアでプリエンプティブで動く処理系は…MultiMLton？使ったことないけど 935 名前：デフォルトの名無しさん mailto:sage [2015/06/21(日) 21:09:48.45 ID:jZdgW1bu.net] >>923 ありがとう！参考にしてみます。 936 名前：デフォルトの名無しさん mailto:sage [2015/06/22(月) 21:17:40.35 ID:NI+fH6po.net] SML/NJにCMLが入ってるみたいだけど 呼び出しかた自体が良く分かりませんでした,,, 937 名前：デフォルトの名無しさん mailto:sage [2015/06/22(月) 22:19:01.14 ID:OHI7eLtz.net] まだバイトコードだけなんで処理速度的にはメリット薄いがocaml-multicoreも開発中 https://github.com/ocamllabs/ocaml-multicore 諦めてF#が一番楽そう 938 名前：デフォルトの名無しさん mailto:sage [2015/07/04(土) 11:48:28.89 ID:D//5Uocc.net] 新潮10月号(9/7発売)に最新長編『モナドの領域』330枚一挙掲載 939 名前：デフォルトの名無しさん mailto:sage [2015/07/19(日) 15:49:50.98 ID:1yK25cK1.net] Haskell　ガチムチいい男 F# タマもサオも取ったニューハーフ OCaml タマは摘出、サオは残したオカマ Java ノン気の一般人 C　古風な一般人 C++ 団塊の世代の一般人 C#　ゆとり世代 940 名前：デフォルトの名無しさん mailto:sage [2015/08/01(土) 08:14:56.43 ID:keSdeN9Q.net] Ocamlってschemeのvaluesに相当するのないのですか？ 941 名前：デフォルトの名無しさん mailto:sage [2015/08/02(日) 05:19:00.73 ID:OeY6iFU6.net] + と+. って絶対に区別しないといけないのです？浮動小数と整数でコードわけるのめんどくさい 942 名前：デフォルトの名無しさん [2015/11/01(日) 12:21:17.11 ID:FL14q5P6.net] min-camlを読み解こうと思ってできれば小さく分けてコンパイルして確かめたいです parser.mly/lexer.mll/id.ml/syntax.ml/type.ml ここまでが最初の塊のようなのでocamlyacc/ocamllexしたあとインタプリタで #use "type.ml" #use "id.ml" #use "syntax.ml" #use "parser.ml" #use "lexer.ml" までやるとlexer.mlを読み込んでいるのにlexer.mllでエラーがでます どうやってインタプリタに読み込めばいいのでしょうか 943 名前：デフォルトの名無しさん mailto:sage [2016/03/06(日) 17:23:06.30 ID:LFfI8YF2.net] C++11とboostでmlと等価なこと出来るようになってない？ 944 名前：デフォルトの名無しさん mailto:sage [2016/03/07(月) 12:29:48.85 ID:IQOnvxBL.net] 楽にはなっても等価にはなってない 945 名前：デフォルトの名無しさん [2016/06/16(木) 23:45:45.68 ID:ogi8+DdB.net] OCaml覚えてHaxeのターゲット自分で書けるようになったらなあって思ったけど パット見何が書いてあるのか良くわからない 946 名前：デフォルトの名無しさん mailto:sage [2016/07/09(土) 07:50:35.12 ID:lXAilHyr.net] >>928 JavaScript 苦労人 947 名前：デフォルトの名無しさん mailto:sage [2016/07/22(金) 00:00:06.57 ID:Zm57F0sF.net] OCaml インストールしてたら �� が出てきた。 絵文字がこんなところにも進出してるとは…… 948 名前：デフォルトの名無しさん mailto:sage [2016/07/23(土) 20:35:22.56 ID:K/hEThar.net] F#はいまいち盛り上がらんのでOCamlに戻るか 949 名前：デフォルトの名無しさん mailto:sage [2016/07/31(日) 08:26:29.15 ID:FitcqrL7.net] OCamlには関数合成がないと訊くんですが、@@は合成ではないのですか 950 名前：デフォルトの名無しさん mailto:sage [2016/09/02(金) 10:19:54.63 ID:75SbB3DN.net] OCaml勉強しはじめの初心者の質問なんですが、どなたか教えてください https://ocaml.org/learn/tutorials/modules.ja.html ここの説明によると、行末の;;を避けるためみんなこう書く open Amodule let () = hello () ってあるんですが、これがまず理解できない ()ってunitの定数値というかリテラルみたいなものなのではないですか？ letで束縛する的なコードが書けることが腑に落ちないのですが・・・ 951 名前：デフォルトの名無しさん mailto:sage [2016/09/02(金) 13:34:30.13 ID:xfbClL/y.net] () って C の void みたいなもんやろ。 hello() の戻り値が void で両辺 void = void で OK みたいな。 952 名前：デフォルトの名無しさん mailto:sage [2016/09/02(金) 18:21:07.36 ID:anKFyHj7.net] =が等号ならそんな感じってするのですが、 let 変数名 = 値　って形に当てはまると unitの()って変数名であり値でもあるってこと？ とか考え出すと混乱して� 953 名前：ｵまいます･･･ [] [ここ壊れてます] 954 名前：デフォルトの名無しさん mailto:sage [2016/09/02(金) 18:22:47.76 ID:h+44ee0t.net] >>939 その用途の場合単なるエントリポイントなので()にそんなに意味はない。 let _ =〜でも動作するよ。 955 名前：デフォルトの名無しさん mailto:sage [2016/09/02(金) 19:39:25.71 ID:MnPjnRyk.net] >>941 letは代入ではなくパターンマッチ 普段は let パターン = 式 のパターンのところに新規の束縛(変数名)を一個置いてるだけ let 1 =2 とか書けてMatch_failureになるよ 956 名前：デフォルトの名無しさん mailto:sage [2016/09/02(金) 21:44:32.31 ID:TuW8Vb/N.net] 皆さんありがとう、何となく分かりました 実際に｢let x::xs = [1;2;3;4];;｣とかやるとx=1、xs=[2;3;4]とかなりますね letってのはmatchの単独パターンバージョンみたいな感じなんですね、きっと 957 名前：デフォルトの名無しさん mailto:sage [2016/09/03(土) 14:38:27.01 ID:xDozGH3Q.net] OCamlも捨てがたい qiita.com/HirofumiYashima/items/98d35b40dde12bbb5d6d 958 名前：デフォルトの名無しさん mailto:sage [2016/09/04(日) 01:00:38.68 ID:m/Nfzz4G.net] たびたび初心者的質問ですいません OCamlにはListやArrayに対するgroup by関数って無いんでしょうか？ 標準ライブラリ(ideoneやyukicoderで利用可能)の範囲内で存在すれば嬉しいんですが･･･ 959 名前：デフォルトの名無しさん mailto:sage [2016/09/04(日) 21:14:26.78 ID:ZFd7dRv3.net] List.filter : ('a -> bool) -> 'a list -> 'a list ならある。 Arrayにはないから自力で実装するかExtLibでも使おう。 っていうか標準ライブラリだったら自分で検索しようね。 馬鹿なの？ 960 名前：デフォルトの名無しさん mailto:sage [2016/09/04(日) 21:40:33.19 ID:m/Nfzz4G.net] >>947 標準ライブラリは探したけど、無かったから自作したよ 最近だとF#にしろscalaにしろgroupbyがあるのが当たり前だから、確認のため聞いてみた その程度の事情も察せないお前が馬鹿じゃねｗ 961 名前：デフォルトの名無しさん mailto:sage [2016/09/05(月) 20:50:26.74 ID:uZnwqH5s.net] 宿題や競プロでもやるんじゃなきゃCoreかBatteries入れないとやってられない 962 名前：デフォルトの名無しさん mailto:sage [2016/09/10(土) 11:17:54.65 ID:hxR4/XV4.net] 標準ライブラリゴミすぎ 963 名前：デフォルトの名無しさん mailto:sage [2016/09/10(土) 20:27:19.82 ID:vL431mpn.net] map reduceに相当するもんがあればいけるんじゃね 964 名前：デフォルトの名無しさん mailto:sage [2017/02/27(月) 20:54:32.60 ID:nBcs47LL.net] 「プログラミングの基礎」を買ってきてOcamlを始めようとしたのですがインタプリタが日本語を表示してくれません。ぐぐっても知識が足らず解決法がわからなくて途方に暮れています。誰か助けて… 965 名前：デフォルトの名無しさん mailto:sage [2017/02/27(月) 21:06:38.41 ID:nBcs47LL.net] 使ってる環境はubuntu16.10です。 966 名前：デフォルトの名無しさん mailto:sage [2017/02/28(火) 21:46:08.53 ID:hBxDt9/3.net] >>952解決しました 967 名前：デフォルトの名無しさん mailto:sage [2017/03/01(水) 12:55:25.91 ID:jLbNtrZK.net] どのようにして解決したのか書いてもらえると 同じ状況に陥った人の助けになるかも知れないわけだが… 968 名前：デフォルトの名無しさん mailto:sage [2017/03/01(水) 16:07:29.52 ID:ZtKy2rs9.net] >>955 解決策を2つ試しました まず、著者のサポートサイト（pllab.is.ocha.ac.jp/~asai/book/Linux.html）を見て、 　�@端末起動→上部メニューバーの端末タブ→文字コードの設定→日本語（EUC-JP）に設定してから 　�ALANG=en_US.ISO88591 ocamlを実行しましたが解決しませんでした。 次に、qiita.com/KenjiYamauchi/items/40aaab56b65777950877を参考にして、 　�@任意テキストエディタで~/（ホームディレクトリ配下の意味）に.ocamlinitというファイルを作り、 　�A「let printer ppf = Format.fprintf ppf "\"%s\"";; 　　 #install_printer printer」と記述した所、解決しました。 コンピュータやプログラミングに詳しい方にはかなりくどいと思いますが、多分自分のようなプログラミング初心者が読む本だと思うので念入りに書いておきます。 969 名前：デフォルトの名無しさん mailto:sage [2017/03/01(水) 16:10:35.17 ID:ZtKy2rs9.net] というか、誰も見てないと思ってた・・・ 970 名前：デフォルトの名無しさん mailto:sage [2017/03/01(水) 16:46:02.21 ID:8oSlLlXA.net] 乙 971 名前：デフォルトの名無しさん [2017/05/01(月) 06:16:47.63 ID:Cn5FkhjE.net] 純粋関数型データ構造が発売されたってのに盛り上がってないな 972 名前：デフォルトの名無しさん mailto:sage [2017/05/01(月) 08:26:08.29 ID:X5RvQ3AI.net] >>959 あれを読むような層は、既に原書で読んでるから気にもしないのでは。 973 名前：デフォルトの名無しさん mailto:sage [2017/05/30(火) 11:59:51.61 ID:heN7Y+lD.net] Real World OCaml で OCaml入門中です。 https://realworldocaml.org/v1/en/html/variables-and-functions.html ... As a result, when passing labeled functions as arguments, you need to take care to be consistent in your ordering of labeled arguments. 要は、ラベル付引数持ちの関数 は 引数の順序気にしなくて良くなるので便利だねって話だったのに、 そういう関数を 他の関数に引数として渡す時は 順序気にしないと型エラーになるかもよ、と。 現 (OCaml ver. 4.04.1) にそうなってるのはしょうがないとして、ユーザーは不満だったりしないんですかね？ 仕様変えてどこでも順序気にしなくてよくなるようにするのは何か不都合があるんでしょうか？ 974 名前：デフォルトの名無しさん mailto:sage [2017/05/31(水) 12:35:03.09 ID:nyiBm3r5.net] はい 975 名前：デフォルトの名無しさん mailto:sage [2017/06/02(金) 14:10:54.16 ID:v4wV8DId.net] >>959 書店で立ち読みしてみたんだけど微妙に扱っているデータ構造少なくね？ サンプルコードがStandard MLというのは驚いたが。 976 名前：デフォルトの名無しさん mailto:sage [2017/06/09(金) 03:43:45.31 ID:Z/PWf/cV.net] 末尾再帰がイメージできないんだけど 977 名前：デフォルトの名無しさん mailto:sage [2017/06/09(金) 10:56:43.72 ID:jgO9PNm3.net] 「なんでも再帰」や「なんでも継続」を読んでみたら？例はSchemeだが 978 名前：デフォルトの名無しさん [2017/06/09(金) 13:37:56.60 ID:3OdcZ+id.net] fact 0 = 1 fact n = n * (fact (n-1)) だと，fact (n-1)の再帰呼出の後で nとの掛け算を しなければならない．計算の最後（＝末尾）が再帰では なく乗算となる． fact2 0 n = n fact2 n k = fact2 (n-1) (n*x) として fact1 n = fact2 n 1 としておけば，fact2の計算の最後はfact2の 再帰呼出で，callをgotoに変えたループで実行できる． こんな感じでイメージできる？ 979 名前：デフォルトの名無しさん mailto:sage [2017/06/09(金) 14:50:46.84 ID:rw1qC18c.net] f_outer(n){ f_inner(n, accumulator){ if 1 == n accumulator else f_inner(n - 1, n * accumulator) } } accumulator に蓄積すれば？ 980 名前：965 mailto:sage [2017/06/09(金) 14:56:24.07 ID:rw1qC18c.net] f_outer(n){ f_inner(n, accumulator){ if 1 == n accumulator else f_inner(n - 1, n * accumulator) } return f_inner(n, 0) } 修正。 内部関数を、return するのが抜けていた 981 名前：デフォルトの名無しさん mailto:sage [2017/06/09(金) 16:51:44.77 ID:VCuqCK40.net] おおおわかった気がする ありがとう！ なんでも再起とやらも読んで見ることにする 982 名前：デフォルトの名無しさん [2017/06/09(金) 17:05:35.04 ID:3Dqy8l+L.net] >>968 return f_inner(n, 1) じゃない？ 983 名前：デフォルトの名無しさん mailto:sage [2017/06/25(日) 18:30:26.47 ID:v1ZjLLZV.net] OcamlとかCoqって名古屋以外でも大学での授業とか研究に使われているの？ 一時期のブームは去ったみたいだけど。 大学の情報学部とかの現状にはちょっとだけ興味がある。 そして流行に後れて今頃勉強している40代のオレ。 984 名前：デフォルトの名無しさん mailto:sage [2017/07/03(月) 09:21:46.88 ID:ipQv+IYB.net] 東大東北大お茶の水では使ってた 985 名前：デフォルトの名無しさん mailto:sage [2017/07/03(月) 17:44:24.93 ID:/M1wO8+Z.net] 授業で使ったのに広まらなかったということか。 つまり啓蒙に失敗したと。 986 名前：デフォルトの名無しさん mailto:sage [2017/07/04(火) 13:46:26.44 ID:VgVQ93XC.net] Occamなら知っとるぞよ？ 987 名前：デフォルトの名無しさん mailto:sage [2017/07/12(水) 14:21:04.56 ID:06OhWRFP.net] >973 広まらなかったというかキラーアプリがなかったというか… 結局Ocamlで作られたアプリで唯一プログラマ間で流行ったのがCoqなんじゃね？ 988 名前：デフォルトの名無しさん mailto:sage [2017/07/12(水) 14:33:02.68 ID:bLDjTsNM.net] OCaml は金融とかで使われてるんじゃ無かったか。 そういや Rust も最初は OCaml でコンパイラー書かれてたんだよな。 989 名前：デフォルトの名無しさん mailto:sage [2017/07/14(金) 23:08:50.92 ID:UJz0OWoz.net] 俺がocaml覚えたきっかけはとあるエロゲーのチートツールなんだが あれの作者がなぜそれを採用したかにはずごい興味ある 990 名前：デフォルトの名無しさん mailto:sage [2017/07/15(土) 12:06:36.80 ID:03i9G/wL.net] >>977 どっかの学生だったんじゃないの？兄妹ものエロゲだけに京大とか。 991 名前：デフォルトの名無しさん mailto:sage [2017/08/16(水) 21:00:55.34 ID:H/HIEf+2.net] (*´・ω・`*) 992 名前：デフォルトの名無しさん mailto:sage [2017/08/17(木) 13:02:39.82 ID:5mQoD0+b.net] (´・ω・｀) 993 名前：デフォルトの名無しさん mailto:sage [2017/09/01(金) 18:43:59.45 ID:RxXe6GrD.net] 8月はちょっと纏まった時間がとれたので、 「ソフトウェアの基礎」日本語訳の練習問題を解きすすめてみた。 まだPoly.vが終わった序盤だけどだいぶCoqに慣れてきた。 星三つrecommendedでもたまに難しい問題があるなー、というのが感想。 論理学の命題というのは高校・大学教育で慣れているだけで 見直してみると思ったよりも複雑な構造をしていたのだと今更ながらに感じた。 実務でCoqが要求されることは当分ないと思うけど、 逆変換の関数は少なからず実装することがあるので ときどき「Coｑ使って証明したい」という気分にはなるんだよなー。 994 名前：デフォルトの名無しさん mailto:sage [2017/09/05(火) 11:03:28.55 ID:a/Cb1ZW9.net] ocaml.jp/ 死んでるな…… > ( ! ) Parse error: syntax error, unexpected 'new' (T_NEW) in /virtual/osiire/public_html/lib/func.php on line 531 995 名前：デフォルトの名無しさん mailto:sage [2017/09/08(金) 14:02:07.35 ID:swD2wqBn.net] ocaml.jpは息してる？ 996 名前：デフォルトの名無しさん mailto:sage [2017/09/24(日) 12:35:45.27 ID:VL5Szw+L.net] いつまで死んでるんだよ 997 名前：デフォルトの名無しさん mailto:sage [2017/10/03(火) 00:31:09.35 ID:JZnIdnEQ.net] 復活した 998 名前：デフォルトの名無しさん mailto:sage [2017/10/03(火) 02:20:47.65 ID:upqeSfz9.net] 復活したのは良いけど、一言何か無いのかよ。誰が管理してるんだ。 999 名前：979 mailto:sage [2017/10/05(木) 12:08:08.18 ID:SZzrAZT5.net] 日本語訳の古さに苦戦しつつLogic.vまで進めていたところ…… 久しぶりに英語の本家を見たら、 なんかVol.1 〜 Vol.3に増えてるー！？ あまりの道のりの遠さに絶望しつつ内容を見ると、 旧版からホーア理論まわりをVol..2に分離し、 Vol.3は赤黒木等の少し高度なデータ構造について色々とCoqで証明して感じらしい（新規）。 ……く、面白そうじゃないか。 1000 名前：デフォルトの名無しさん mailto:sage [2017/10/05(木) 19:45:51.56 ID:72rIdNeW.net] >>981 リンクpls 1001 名前：デフォルトの名無しさん mailto:sage [2017/10/07(土) 12:06:25.63 ID:689sKi0/.net] >>988 https://softwarefoundations.cis.upenn.edu/ 1002 名前：979 mailto:sage [2017/10/30(月) 19:39:25.32 ID:asGH9s/c.net] ここ一ヶ月、旧くなった日本語版を捨て英語版に再挑戦してみた。 以前は出来るだけ写経していたが時間がかかり過ぎるので、 付属の.vファイルを直接書き換える方針に変更。 結構章立てと共に内容変わってるなぁ……追加された良問も多いし。 英語の非形式的証明は書く機会もなさそうだし、パスするか。 しかし、答えがWeb上に転がってないのは自習者には正直辛い。 どうもSICPみたいな標準教科書を目指してるっぽい？ こーゆうの(coq)を国立研究所で作れる国はやっぱり凄いと思う今日この頃。 1003 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:27:01.78 ID:wuKEf1Sh.net] a 1004 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:27:36.60 ID:wuKEf1Sh.net] sit 1005 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:27:56.41 ID:wuKEf1Sh.net] dot 1006 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:28:13.79 ID:wuKEf1Sh.net] egg 1007 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:28:31.25 ID:wuKEf1Sh.net] nø 1008 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:28:48.81 ID:wuKEf1Sh.net] this 1009 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:29:26.33 ID:wuKEf1Sh.net] combi 1010 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:30:08.09 ID:wuKEf1Sh.net] it 1011 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:30:42.85 ID:wuKEf1Sh.net] 2 1012 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:31:16.98 ID:wuKEf1Sh.net] ping 1013 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:32:05.81 ID:wuKEf1Sh.net] pong 1014 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:32:32.73 ID:wuKEf1Sh.net] wild 1015 名前：1001 [Over 1000 Thread.net] このスレッドは１０００を超えました。 新しいスレッドを立ててください。 life time: 3061日 0時間 17分 11秒 1016 名前：過去ログ ★ [[過去ログ]] ■ このスレッドは過去ログ倉庫に格納されています

---

---

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

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