はてなブックマーク

プログラミング in OCaml 〜関数型プログラミングの基礎からGUI構築まで〜 (GIHYO Digital Publishing, amazon, 楽天Kobo, yahoo, cbook24.com) PDF/EPUB 版を販売しているGIHYO Digital Publishing のページ おしらせ EPUB版が GIHYO Digital Publishing, Amazon, 楽天Koboで販売開始です．GIHYO Digital Publishing だと pdf とのセット販売(価格は同じ)です． (2014.12.10) 長い間，出版社在庫切れとなっていましたが，この度，細かい修正を施した pdf 版の販売を GIHYO Digital Publishing にて開始しました．価格は 1,400 円と冊子体の半額です! (2012.08.29) 第16章のプログラム

[ 前の資料 | 講義ホームページ・トップ | 次の資料 ] 2018年度未改訂 Lisp Lisp は John McCarthy1 によって提案されたFORTRAN についで古い高水準プログラミング言語である．数々の方言とその実装があるが，特に有名なものは Common Lisp と Scheme である．"Lisp" は，ひとつのプログラミング言語というよりも，以下のような共通の特徴を持った言語族を表す名前といったほうがよいかもしれない． S式に基づく括弧を多用した前置記法構文 動的型付け: (ふつうは)コンパイラによる型検査がないが，実行時にデータの種類(これも型と呼ばれる)を調べることができる 自動メモリ管理(ガーベジコレクション) コンスセルを使った汎用的なデータ構造表現 ここでは Scheme の簡単な紹介をしながら2分探索木のプログラムまで見ていく．Scheme の処理系も

[ 前の資料 | 講義ホームページ・トップ | 次の資料 ] Java Java の主要概念の復習(超特急版) オブジェクト インスタンス変数の集まりからなるデータとそのデータに対する操作(メソッド)の集まり． インスタンス変数 オブジェクトに格納されるデータを表すための変数． メソッド オブジェクト内のデータに対する操作．メソッドが呼出されると，呼出し元から与えられる引数とインスタンス変数を使って計算を行う．場合によってはインスタンス変数の値を代入によって更新する．最終的に何らかの計算結果を呼出し元に返す(ことが多い)． シグネチャ メソッドの名前，引数の個数とそれぞれの型，返り値の型をまとめて，メソッドのシグネチャと呼ぶ．シグネチャさえわかれば，そのメソッドをどういう形式で呼出せばよいかわかる． クラス オブジェクトの定義を与えるプログラム構成単位．インスタンス変数の宣言，インスタンス

[ 前の資料 | 講義ホームページ・トップ | 次の資料 ] OCaml OCaml (旧名称: Objective Caml)は INRIA というフランスの国立の計算機科学の研究所でデザイン・開発された言語である．歴史的には，証明支援系と呼ばれる，計算機によって数学的証明を行うためのソフトウェアを操作するための言語の研究から発展してきたもので，当初は ML (Meta Language) と呼ばれていたが，研究が進展し，また方言が派生していく過程で OCaml ができあがった．Standard ML などの方言をまとめて ML と呼ぶことが多い．(興味があったら Caml の歴史, Standard MLの歴史 などを見よ．) ML は関数型プログラミング(functional programming)と呼ばれるプログラミングスタイルをサポートしている．MLは核となる部分が小さくシンプ

五十嵐 淳 (京都大学大学院情報学研究科 通信情報システム専攻) 2017年11月17日 モジュールと実装の隠蔽 階層的名前空間の提供 実装の隠蔽 分割コンパイル (ocaml/bstModule2) 講義範囲を越えて [ 前の資料 | 講義ホームページ・トップ | 次の資料 ] モジュールと実装の隠蔽 モジュール(module) とは，工業製品などにおける規格化された構成単位を指すための用語である．要するに部品のことなのだが，この「規格化」というのは重要な点で，これによって例えば様々な会社が製造した部品を集めてひとつの大きな製品を作ることができるし．一部が故障しても簡単に交換することが可能になる．ソフトウェアにおいても，モジュールという用語はプログラム部品の構成単位を指していて，多くのプログラミング言語が，プログラムをモジュールの集まりとして構成するための支援機構を用意している．工業製品

ここでは <式> の代わりに e という記号(メタ変数)，<識別子> の代わりに x という記号(メタ変数)を用いている． また，型(メタ変数 τ)として，整数を表す int, 真偽値を表す boolを考える． さて，型推論のアルゴリズムを考える前に，そもそも「式 e が型 τ を持つ」という関係がどのような時に成立するかを正確に記述したい． 例えば「式 1+1 は型 int を持つ」だろうが， 「式 if 1 then 2+3 else 4 は型 int を持つ」は 成立しないと思われる．この，「式 e が型 τ を持つ」 という判断を型判断(type judgment)と呼び，e : τ と略記する． しかし，一般に式には変数が現れるため，例えば単に x が int を持つか，といわれても判断することができない．このため，変数に対しては，そ れが持つ型を何か仮定しないと型判断は下せない

ここでは <式> の代わりに e という記号(メタ変数)，<識別子> の代わりに x という記号(メタ変数)を用いている． また，型(メタ変数 τ)として，整数を表す int, 真偽値を表す boolを考える． さて，型推論のアルゴリズムを考える前に，そもそも「式 e が型 τ を持つ」という関係がどのような時に成立するかを正確に記述したい． 例えば「式 1+1 は型 int を持つ」だろうが， 「式 if 1 then 2+3 else 4 は型 int を持つ」は 成立しないと思われる．この，「式 e が型 τ を持つ」 という判断を型判断(type judgment)と呼び，e : τ と略記する． しかし，一般に式には変数が現れるため，例えば単に x が int を持つか，といわれても判断することができない．このため，変数に対しては，そ れが持つ型を何か仮定しないと型判断は下せない

2012年1月14日のジュンク堂書店池袋本店トークセッション「新春座談会 このコンピュータ書がすごい！ 2012年版〜2011年に出たコンピュータ書ならこれを読め！〜」にて本書が紹介された模様です．(2012/1/14記)補助資料正誤表演習システムガイド継続(EvalContML1)第一級継続(EvalContML4)参照(EvalRefML3)本演習システムを使っている講義京都大学 大学院情報学研究科 通信情報システム専攻 専門科目「プログラム意味論」(2013年度〜)京都大学 大学院情報学研究科 知能情報学専攻 専門科目「ソフトウェア基礎論」(2008年度〜2012年度)お茶の水女子大学 大学院人間文化創成科学研究科 理学専攻 情報科学コース「言語意味論」(2012年度)お茶の水女子大学 理学部 情報科学科「計算モデル論」(2012年度)Updated on 2022-05-25 21

2012年1月14日のジュンク堂書店池袋本店トークセッション「新春座談会 このコンピュータ書がすごい！ 2012年版〜2011年に出たコンピュータ書ならこれを読め！〜」にて本書が紹介された模様です．(2012/1/14記)補助資料正誤表演習システムガイド継続(EvalContML1)第一級継続(EvalContML4)参照(EvalRefML3)本演習システムを使っている講義京都大学 大学院情報学研究科 通信情報システム専攻 専門科目「プログラム意味論」(2013年度〜)京都大学 大学院情報学研究科 知能情報学専攻 専門科目「ソフトウェア基礎論」(2008年度〜2012年度)お茶の水女子大学 大学院人間文化創成科学研究科 理学専攻 情報科学コース「言語意味論」(2012年度)お茶の水女子大学 理学部 情報科学科「計算モデル論」(2012年度)Updated on 2022-05-25 21

自習の進め方(宿題について) 教科書の該当する章のファイルを Proof General (もしくは CoqIDE) で読み込む． Coq への読み込みコマンドを使いながら教科書を読み進める． 練習問題の指示に従ってファイルを書き換える(解答を埋める)． (* FILL IN HERE *) Admitted. の行を消して，証明を書く． (最初の方の問題について書くべき「証明」は決まっている．) わからない問題については，Admitted. を残しておく．(証明途中で詰まった場合でも， 全部消さずに，最後に Admitted. を書いておく．) Coq に読み込ませてみて，背景が青(緑)になれば無事に Coq のチェックに通った，ということ．ただし， Proof General, CoqIDE は Qed. の打ち忘れ(よくある!)を関知してくれないので，make XXXX.vo (XX