…「指標とヒルベルト・イプシロン記号を利用しよう」で導入した $`\ClassOf{\hyp}`$ を使います。 名前 $`\mrm{Injection}`$ は、指標の名前である。 それと同時に、名前 $`\mrm{Injection}`$ は型の名前でもある。 $`\ClassOf{\mrm{Injection}}`$ は、型 $`\mrm{Injection}`$ の実例の集合を表す。 型理論では、$`x`$ が 型 $`T`$ の実例であることを $`x:T`$ と書く…

…「指標とヒルベルト・イプシロン記号を利用しよう」では、シンボルとして $`\T{'field of fractions'}`$ を名前に使ったりしているし。さらに安全性（事故の起こりにくさ）を気にするなら、表示では大文字小文字混ぜて空白をいれてもいいが、正規化手順があり、正規化して同じ名前は許さないとします。正規化の手順は： 大文字はすべて小文字に変換 空白はハイフンに置き換える 例えば、field of fractions と Field-of-fractions は同じ文…

…ですが、ヒルベルトのイプシロン記号も使用すべき場面は多いようです。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{\text{ in }} %\newcommand{\o}[1]{\overline{#1}} \newcommand{\hyp}{\text{－} } %\newcommand{\twoto}{\Rightarrow } \newcommand{\Imp}{\Rightarrow } \newcomm…

… 指標とヒルベルト・イプシロン記号を利用しよう デジタル語彙目録:: 名前の管理 名前が指すモノ： 単射を例として デジタル語彙目録:: こんな感じ（中間報告） デジタル語彙目録:: 野生の言葉達と索引 デジタル語彙目録:: Obsidian Publish によるWeb公開 語彙目録の用途・目的語彙目録〈lexicon〉とは、辞書、索引、用語集のような、用語〈専門用語〉の説明を集めたものです（「同義語・多義語の問題： タグによる修飾と分類」参照）。用語の説明を与える単位が語…

…数 $`y`$ に、イプシロン記号で作られた選択関数の値を代入することを示します。この表現は、だいたい次の英語の文に相当します。$`\quad y \text{ is a } x_1 \text{ such that } P(x_1, \cdots, x_n)`$変数 $`x_1`$ はイプシロン記号で束縛されているので、同じ名前の自由変数を使っても問題ありません。$`\quad x_1 := \varepsilon\, x_1. P(x_1, \cdots, x_n)`$変…

…の一部をヒルベルトのイプシロン記号で説明することを目標にします。その準備として、型クラス述語という概念を導入します。$`\newcommand{\cat}[1]{ \mathcal{#1}} \newcommand{\mrm}[1]{ \mathrm{#1}} \newcommand{\In}{ \text{ in }} \newcommand{\Imp}{ \Rightarrow } \require{color} % 緑色 \newcommand{\Keyword}[1]…

…ます。（ヒルベルトのイプシロン記号を使っています。）$`\For a, b\in X\\ \quad a \wedge b := \varepsilon x\in X.\, \mrm{IsMeet}(x, a, b) `$こうして定義した二項演算は次の法則を満たします。 $`(a \wedge b) \wedge c = a \wedge (b \wedge c)`$ $`a \wedge b = b \wedge a`$ $`a \wedge a = a`$ これは、ベキ等…

…の命題をヒルベルトのイプシロン記号を使って書いてみます。イプシロン記号については次の過去記事参照。 イプシロン計算ってなんですかぁ？ こんなもんですよぉ 命題をちゃんと書くとけっこう複雑です*2。$`\Name{定理} (\exists y \in X.\, \mrm{IsLeast}(y, P)) \Imp \mrm{IsLeast} (\varepsilon y\in X.\,\mrm{IsLeast}(y, P) , F) `$これを示しましょう。 証明 [追記]「証明…

…定した集合ではないような印象はあります。集合とは限らない類〈class〉に値をとる場合が族の雰囲気。このテの話を、印象・雰囲気で議論してもラチがあかないので、やめときます。 *4:厳密には、Map(A, X)のXは、忘却関手をUとして U(X) です。集合圏とベクトル空間の圏のあいだの随伴関手対があるのです。 *5:自然変換や圏論的オペレータです。 *6:directCoeffの定義を形式言語でしようとすると、述語論理の論理式以外にヒルベルトのイプシロン記号が必要になります。

イプシロン記号／イプシロン記法／イプシロン計算については何度か述べたことがあります。今回は、イプシロンを実用的に使うための補助構文について述べます。ここで述べるアイディアは、証明検証系Mizarから拝借しています。ただし、Mizarそのものには触れませんし、Mizarの知識も不要です。 内容： 関数の書き方 イプシロン記法 イプシロン項の基本性質 イプシロン項の不定性 イプシロン項による関数定義 関数の余域を制限する 関数の書き方中学校で習う1次関数は、 y = 2x + 1…

… モノイドの単位元 イプシロン記号 一意存在と一意イプシロン記号 一意イプシロン項と名前の導入 一意イプシロン項と名前の消去 0と1を定義してみよう モノイドの単位元Aは集合で、m:A×A→A を写像とします。mはA上の二項演算ですね。このmは結合律を満たすとしましょう。登場する変数x, y, zなどは集合A上を走るとします。 ∀x, y, z.(m(m(x, y), z) = m(x, m(y, z))) --- 結合律 結合律に加えて単位元が存在すれば、Aはモノイドになり…

…持つ共通の特性です。イプシロン記号εも束縛子です。限量子と同じように、論理式Fに対して εx.F を作れます。集合の内包的表記法 {x | F} もイプシロン記号と似た束縛子になっています。論理式Fを、真偽値を値とする関数の表現と考えると、ラムダ式 λx.F が定義する関数は、集合 {x | F} の特性関数になっています。部分集合と特性関数を同一視するなら、内包的表記法はラムダ束縛と同じことです。式Eで定義される関数の最小不動点を表す μx.E も束縛子です。最大不動点なら…

…数を構成するここで、イプシロン記号を思い出してください。 イプシロン計算ってなんですかぁ？ こんなもんですよぉ Pが変数xを含む命題として、εx.P は、「Pであるようなx」と読みます。∃!x.P は「Pであるようなxが一意的に存在する」ことを意味します。命題Pが変数yを含んでいて、もし ∀y.(∃!x.P) が証明できているなら、次の式で関数fを定義できます。 f(y) = εx.P ただし、xやyが動く範囲は前もって明確にしておく必要があります。我々は、disjoint-…

… 随伴の例 ε記号〈イプシロン記号〉はヒルベルトあたりが導入したんじゃないのかな、よく調べてないけど。ところで、再帰的計算に関連してμ（ミュー）やν（ニュー）という記号が出てきますが、これはεと似たようなものです。そのことをちょっと述べておきます。内容： 集合の内包的記法 ε記号 μ記号 ν記号 集合の内包的記法Pがなんらかの条件を表す論理式のとき、{x∈X | P(x)} という書き方はよく使われます。集合の内包的記法ですね。Xをあらかじめ決めて固定しておけば、{x | P…

…。次のイプシロン項（イプシロン記号を使った項）は、リースの表現定理のおかげで意味を持ち、fごとにaを定めます。 εa.∀x.(f(x) = (x|a)) λf.εa.∀x.(f(x) = (x|a)) というイプシロン・ラムダ項は H*→H という関数（写像）を定義しますが、これは線形ではなくて反線形です。その形から、Ψ = λa.λx.(x|a) : H→H* という反線形写像の逆であることがわかります。 Ψ-1 = λf.εa.∀x.(f(x) = (x|a)) H*→H…

…しましょう。内容： イプシロン記号とイプシロン項 イプシロン項の意味 イプシロン項が定義する関数 例題：gがfの断面（セクション）であること イプシロン記号とイプシロン項負の数-1とか、無理数√2とかを導入するとき、次のような定義をしましたよね。 -1とは、x + 1 = 0 であるようなx 2の平方根とは、x2 = 2 であるようなx（のひとつ） √2とは、x2 = 2 かつ x ≧ 0 であるようなx ここで、「…であるようなx」という表現が登場します。これを、εx.(……