プログラミングの基礎理論 第4回 自由に生成された集合と再帰的関数、暗黙に型付けられたラムダ計算
はじめに 帰納的閉包のさらなる理解のために、 自由に生成された集合 再帰的関数定義 について理解するのが良いので概要のみ紹介する。 自由に生成された集合 帰納的閉包 X = Ind(C, F)が以下の条件を満たすとき、「自由に生成された集合である」と言う。 任意の異なる関数fr(n),gr(m) ∈ Fに対して、fr(n)(X) ∩ gr(m)(X) = ∅ である。 1.1 つまり異なる関数を適用した結果の共通集合はなく、すなわち異なる関数を適用した結果はそれぞれ異なることを意味する 任意の関数fr(n) ∈ Fについて、fr(n)(X) ∩ C = ∅ である 2.1 つまり関数を適用した場合、定数Cを生成することはないことを意味する 任意の関数fr(n) ∈ Fについて、fr(n)|xn は単射関数である 3.1 fのXへの制限すなわち定義域をXに制限した集合{(a, b) | (a
プログラミングの基礎理論 第2回 言語の帰納的な定義
はじめに Twitterにてこのようなツイートを見かけたので、内容を確認してみた。 これまでインターネットや書籍で軽く触れられてきた内容に切り込んでいくものだったので、理解を深めることができた。 その内容をまとめていく。 概要 言語は文法で定義される。 例えば、MLの一部の式は以下のように定義される。 <exp> ::= <id> // 変数 | <n> | <S> | true | false // 自然数(n), 文字列(S) その他定数 | fn <id> => <exp> // 関数式 | <exp> <exp> // 関数適用 | ... プログラミング言語の理論ではより抽象的な定義を行うため、変数や定数を「与えられた集合」とし、これを代表するものをメタ変数と呼ぶ。 ラムダ式では以下の集合とメタ変数を導入する。 変数(Var)に対するメタ変数をxとする 定数(Const)に対する
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
