東洋文化研究会 論考 令和8年4月15日
EML演算子のMartin-Löf型理論による再定式化と
無極・絶対矛盾的自己同一・易の生成原理との構造的統合
抄 録
Odrzywołek(2026)は、単一の二項演算子 $\mathrm{eml}(x,y)=\exp(x)-\ln(y)$ と定数 $1$ のみから、科学計算機が扱う全初等関数を構成的に導出できることを示した。本稿はこの結果を出発点として、三つの方向への拡張を試みる。第一に、EML体系をMartin-Löf直観主義型理論(MLTT)の枠組みで再定式化し、宇宙階層 $\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : \cdots$ を導入することで「EML式の全体」という対象の存在論的地位を型論的に精確に定める。第二に、EMLが生成しうる対象の総体 $\mathcal{U}_{\mathrm{EML}}$ を真クラス(proper class)として定位し、これがZFC集合論における単純な集合として扱えない理由を示す。第三に、この構造的分析を通じて得られた四層図式(無極・太極・陰陽・万物)が、周敦頤の宇宙生成論、西田幾多郎の「絶対矛盾的自己同一」、およびMLTT宇宙階層の三者と構造的に同型であることを論じる。本稿の主張は、いずれも比喩的類比にとどまらず、各概念の形式的定義に基づく構造的対応として提示される。
§1 序論
デジタル回路においては、単一の二入力ゲートNAND(Sheffer 1913)が全ブール論理を生成するという事実は古くから知られている。これに対応する連続数学の基本演算が存在するかどうかは長らく未解決であったが、Odrzywołekは2026年の論文において、この問いに対する肯定的な答えを提出した[1]。
その基本演算は次のように定義される:
$\mathrm{eml}(x,\,y) \;=\; \exp(x) – \ln(y)$
この演算子と定数 $1$ のみから、$\sin, \cos, \sqrt{\phantom{x}}, \pi, i, e$ を含む全初等関数が、文法 $S \to 1 \mid \mathrm{eml}(S,S)$ に従う有限の二分木として構成的に表現できる。Odrzywołekはこれを「連続数学のSheffer元」と呼んでいる。
本稿はこの体系に対して三つの問いを立てる。
問い1(型論的地位):「EMLで生成可能な全式の総体」という対象を、矛盾なく数学的に扱うにはいかなる枠組みが必要か。
問い2(真クラス問題):この総体を集合として扱おうとすると何が問題となり、それを真クラス(proper class)として定位することでどのように解消されるか。
問い3(哲学的統合):上記の型論的構造は、周敦頤の無極論、西田幾多郎の「絶対矛盾的自己同一」、および易の陰陽生成論と、いかなる構造的関係にあるか。
これらの問いに答えるため、本稿はまずMLTTの宇宙階層理論(§2)を概観し、EML体系のMLTT再定式化(§3)を展開する。次に真クラスとしての $\mathcal{U}_{\mathrm{EML}}$ を定義し(§4)、四体系の構造的統合論(§5)を提示する。最後に残された問題と展望を述べる(§6)。
§2 Martin-Löf型理論の宇宙階層
2.1 基本概念
Martin-Löf直観主義型理論(MLTT)は、1972年にPer Martin-Löfが提唱した構成的数学の基礎体系である[2]。MLTTの特徴は、命題と型を同一視するCurry-Howard対応にあり、証明は型の要素(項)として構成的に与えられる。
MLTTの初期版(MLTT71)は「型の型」を許す規則 $\mathsf{Type} : \mathsf{Type}$ を持っていたが、Jean-Yves Girardはこれが矛盾を生む(Girardのパラドックス)ことを示した[3]。これはちょうど、集合論においてすべての集合の集合 $\{x \mid x = x\}$ を許すとRussellのパラドックスが生じるのと構造的に類比的である。
この問題を解決するために、Martin-Löfは1975年の論文において宇宙 $\mathsf{U}$ を導入し、宇宙は自分自身を要素として含まないよう制限した[4]。さらにMLTT73では宇宙の無限階層が導入された:
$\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : \cdots$
定義 2.1(宇宙階層)
MLTTにおける宇宙の累積的階層とは、型の列 $\{\mathcal{U}_i\}_{i \in \mathbb{N}}$ であって以下を満たすものである:
(i)各 $\mathcal{U}_i$ は型であり、$\mathcal{U}_i : \mathcal{U}_{i+1}$(上位宇宙に属する)。
(ii)$A : \mathcal{U}_i$ ならば $A : \mathcal{U}_{i+1}$(累積性)。
(iii)$\mathcal{U}_i \notin \mathcal{U}_i$(各宇宙は自分自身を含まない)。
Palmgren(1998)はこの宇宙階層の概念を拡張し、超宇宙(superuniverse)を導入した[5]。超宇宙は集合論における到達不可能基数(inaccessible cardinal)と類比的であり、型理論における「大きな全体」を扱う手段を提供する。
2.2 宇宙多形性と型的安全性
宇宙階層の実践的意義は、宇宙多形性(universe polymorphism)にある。任意のレベル $\ell$ に対して定義される型は、より高いレベルでも自動的に有効となる。Agda(Nordfalkらが開発)やCoq(Rocq)はこの機構を実装している[6]。
定理 2.2(Girardのパラドックス回避)
宇宙階層 $\mathcal{U}_0 : \mathcal{U}_1 : \cdots$ を採用し、各宇宙が条件(iii)を満たすとき、「型の型」による自己言及的矛盾は生じない。
証明の概要:$\mathcal{U}_i : \mathcal{U}_{i+1}$ であるから、$\mathcal{U}_i$ について話すとき、私たちは常に $\mathcal{U}_{i+1}$ 以上のレベルにいる。$\mathcal{U}_i \notin \mathcal{U}_i$ により、宇宙が自分自身の要素となる循環は禁じられる。Nordström・Petersson・Smith(1990)を参照[7]。
§3 EML体系のMLTT再定式化
3.1 EML式の型論的定義
Odrzywołekの文法 $S \to 1 \mid \mathrm{eml}(S,S)$ をMLTTの枠組みで再定式化する。まず、複素数体 $\mathbb{C}$ を型として定める。論文が明示するように[1]、emlは $\pi$ や $i$ の生成に $\ln(-1)$ を要するため、複素数域での演算が不可欠である。
定義 3.1(EML型)
宇宙 $\mathcal{U}_0$ において、帰納型 $\mathrm{Expr}$ を以下の構成子で定める:
$\mathrm{eml} \;:\; \mathrm{Expr} \to \mathrm{Expr} \to \mathrm{Expr}$
この帰納型は $\mathcal{U}_0 : \mathcal{U}_1$ を満たす。すなわち $\mathrm{Expr}$ は $\mathcal{U}_0$ に属する型であり、$\mathcal{U}_0$ 自体は $\mathcal{U}_1$ の要素である。
次に、EML式の意味論として評価関数 $\mathrm{eval}$ を定める:
$\mathrm{eval} \;:\; \mathrm{Expr} \to \mathbb{C}$
$\mathrm{eval}(\mathrm{one}) \;=\; 1$
$\mathrm{eval}(\mathrm{eml}(s,\,t)) \;=\; \exp(\mathrm{eval}(s)) – \ln(\mathrm{eval}(t))$
Odrzywołekの主定理はMLTTの枠組みで次のように再定式化される:
定理 3.2(EML完全性、MLTT版)
任意の初等関数 $f : \mathbb{C}^n \to \mathbb{C}$(ただし $f$ は Odrzywołek の Table 1 が定める36個の基本関数のいずれか)に対して、$\mathrm{Expr}$ の項 $e$ が存在し、$\mathrm{eval}(e) \equiv f$ が計算的に等しい。
証明: Odrzywołek(2026)§3 の構成的証明による[1]。各関数の表現式はAgdaプログラムに相当する有限の $\mathrm{Expr}$ 項として与えられる。
3.2 定数 $1$ の型論的地位
定数 $1$(構成子 $\mathrm{one}$)の型論的地位は特殊である。$\ln(1) = 0$ であることから、$\mathrm{one}$ は $\mathrm{eml}(x, \mathrm{one}) = \exp(x) – 0 = \exp(x)$ という中性化作用を持つ。これは帰納型における「基底ケース」(base case)に対応し、再帰の停止条件を与える。
命題 3.3($\mathrm{one}$ は計算的零元)
$\mathrm{eval}$ の定義において、$\mathrm{one}$ は対数項を消去する役割を担う中性元であり、この性質なしに $\mathrm{exp}$ の独立した生成は不可能である。
3.3 $\mathrm{eml}$ の非対称性の型論的解釈
$\mathrm{eml}(x,y) \neq \mathrm{eml}(y,x)$ という非対称性は、MLTTの依存型として自然に捉えられる。$\mathrm{eml}$ の第一引数は $\exp$ によって扱われ(拡張的・発散的方向)、第二引数は $-\ln$ によって扱われる(収束的・制約的方向)。この役割の非対称性は、依存型 $\Pi_{(x:\mathrm{Expr})}(\mathrm{Expr} \to \mathrm{Expr})$ として型付けられる際に、二つの引数位置が構造的に区別されることに対応する。
§4 真クラスとしての $\mathcal{U}_{\mathrm{EML}}$ と無極
4.1 問題の設定
§3で定義した $\mathrm{Expr}$ は $\mathcal{U}_0$ に属する帰納型である。$\mathrm{Expr}$ 自体は有限の二分木の(可算無限個の)集合として問題なく扱える。しかし、ここで問題となるのは「EMLが意味論的に到達しうる全対象の総体」という概念である。
EMLの演算域は $\mathbb{C}$ であり、$\mathbb{C}$ 上の全関数空間、さらにその上の関数空間……と考え始めると、これは集合論的宇宙 $V$ の断片に触れ始める。ZFC集合論において、この「全体」は集合として定義できない。
定義 4.1(EML宇宙クラス)
$\mathcal{U}_{\mathrm{EML}}$ を「$\mathrm{eml}$ 演算子の反復適用によって意味論的に表現可能な全数学的対象の総体」として定義する。形式的には:
4.2 $\mathcal{U}_{\mathrm{EML}}$ が集合でない理由
命題 4.2
定義 4.1 の $\mathcal{U}_{\mathrm{EML}}$ は、ZFC集合論の意味での集合ではなく、真クラス(proper class)である。
論証:
(i)Cantorの定理との衝突:もし $\mathcal{U}_{\mathrm{EML}}$ が集合 $S$ であるとする。すると $S$ 上の全関数の集合 $S^S$ は $|S^S| > |S|$ を満たす(Cantorの定理)。しかし EML は $S^S$ の要素である関数をも(適切な拡張によって)表現できるはずであり、これは $S^S \subseteq \mathcal{U}_{\mathrm{EML}} = S$ と $|S^S| > |S|$ とが矛盾する。
(ii)全初等関数空間の問題:EMLが生成する対象の中に「任意の $n$ に対して $n$-変数初等関数」が含まれる場合、これらの全体は単一の集合として整合的に扱えない。
(iii)MLTT宇宙での対応:MLTTにおいて、「全ての宇宙 $\mathcal{U}_i$ の要素である型の全体」は、いかなる固定された $\mathcal{U}_n$ にも属さない。これが型論における真クラス相当物であり、$\mathcal{U}_{\mathrm{EML}}$ はこれに対応する。
4.3 無極との構造的対応
周敦頤の『太極図説』冒頭「無極而太極」における「無極」の解釈は歴史的に争われてきた。朱熹(1130–1200)は「無極とは太極の形なき状態を指す修飾語であり、太極と別の実体ではない」と解した[8]。これに対し陸象山(1139–1193)は「無極という語は不要であり、太極一語で足りる」と反論した。
本稿は朱熹的解釈に型論的根拠を与える:
命題 4.3(無極の型論的定位)
無極を「EML体系が生成しうる全対象の総体 $\mathcal{U}_{\mathrm{EML}}$(真クラス)」として解釈するとき、以下が成立する:
(i)$\mathcal{U}_{\mathrm{EML}}$ は演算子 $\mathrm{eml}$(太極)の操作対象ではなく、その「場所」である。
(ii)$\mathcal{U}_{\mathrm{EML}}$ に対して $\mathrm{eml}$ を適用することはできない($\mathcal{U}_{\mathrm{EML}} \notin \mathcal{U}_{\mathrm{EML}}$)。
(iii)この不可操作性が「無極」——いかなる規定(極)も受け付けない全体——の数学的表現である。
西田の「絶対無」との対応もここに現れる。西田は「場所」を「自己自身を無にして無限の有を含むもの」と規定したが[9]、$\mathcal{U}_{\mathrm{EML}}$ はまさに「自ら対象とはならないが、全対象を含む場所」として機能する。
§5 四体系の構造的統合
5.1 四層対応図式
以下の表は、易の宇宙生成論・MLTT宇宙階層・EML体系・西田哲学の四体系における、構造的に対応する概念を示す。
| 層 | 易(周敦頤) | MLTT宇宙階層 | EML体系 | 西田哲学 |
|---|---|---|---|---|
| 第零層 | 無極 (規定不能な全体) |
$\mathcal{U}_\omega$(全宇宙の極限) 真クラス相当 |
$\mathcal{U}_{\mathrm{EML}}$ (真クラス) |
絶対無 (場所の論理的基底) |
| 第一層 | 太極 (生成の源一) |
$\mathcal{U}_0 : \mathcal{U}_1 : \cdots$ (宇宙形成規則) |
$\mathrm{eml}(x,y)$ (単一二項演算子) |
絶対矛盾的自己同一 (生成の動的原理) |
| 第二層 | 陰陽 (非対称双対) |
$\Pi$-型 / $\Sigma$-型 (依存型の双対) |
$\exp(x)$ / $-\ln(y)$ (発散 / 収束) |
個(多)/ 世界(一) の逆対応 |
| 第三層 | 万物 (六十四卦・個物) |
$\mathcal{U}_0$ の要素 (具体的型・項) |
$\mathrm{Expr}$ の項 (有限EML式) |
個物 (世界の構成要素) |
表1:四体系の四層構造的対応
5.2 共有される三つの形式的パターン
パターンI:最小生成元の存在
四体系すべてにおいて、体系全体の多様性を生み出す「最小限の生成元」が存在する。EMLにおける $\mathrm{eml}$ と定数 $1$ は、Odrzywołekが示したとおり理論的下限である(二項演算子1つ+終端記号1つ以上の削減は不可能)[1]。MLTTにおける宇宙形成規則 $\mathcal{U}_i : \mathcal{U}_{i+1}$ は、型の階層全体を一つの再帰規則から生む。易においては陰(⚋)と陽(⚊)の二値が六十四卦の完全な基底をなす。西田においては「絶対矛盾的自己同一」という単一の動的原理が個物の世界全体を生成する。
パターンII:非対称双対性
各体系の生成元は、対称ではなく非対称な双対的構造を内包する。$\mathrm{eml}(x,y)$ は第一引数に $\exp$(拡張)、第二引数に $-\ln$(制約)を割り当て、これは可換ではない。易において陰陽は相補的であるが、「太極動いて陽を生じ、静じて陰を生ず」(周敦頤)という記述は動(陽)が静(陰)に先行する非対称性を示す[10]。西田の「個と一般の逆対応」は、個が一般を限定すると同時に一般が個を限定するという、方向を持った双方向的緊張である[11]。MLTTの $\Pi$-型と $\Sigma$-型は双対的だが、それぞれ全称と存在という非対称な量化論理に対応する。
パターンIII:再帰的自己展開と全体の不可対象化
生成則の反復適用が原理的に無限の表現空間を開く一方、その「全体」は生成則自身の適用対象にはなれない。EMLにおいては $\mathcal{U}_{\mathrm{EML}} \notin \mathcal{U}_{\mathrm{EML}}$(§4)。MLTTにおいては $\mathcal{U}_i \notin \mathcal{U}_i$(定義2.1(iii))。西田において「世界は個物を生み出すが、世界自体は一つの個物ではない」[12]。易において六十四卦は有限だが、その変化(変易)の過程は原理的に無限である。この「全体の不可対象化」こそが、前節で論じた真クラス・絶対無・無極の共通構造である。
5.3 西田「絶対矛盾的自己同一」のEML的読解
西田は1939年の論文で次のように述べる:
「現実の世界は何処までも多の一でなければならない、個物と個物との相互限定の世界でなければならない。故に私は現実の世界は絶対矛盾的自己同一というのである。」[11]
この「多と一の絶対矛盾的自己同一」をEML体系に読み込むと次のようになる。個々のEML式($\mathrm{Expr}$ の項=多)は互いに区別される有限の対象である。しかし全ての式は同一の $\mathrm{eml}$ ノードの入れ子として構成される(一)。この「多即一・一即多」の構造が $S \to 1 \mid \mathrm{eml}(S,S)$ という文法に現れている。文法は「一」(単一規則)であり、その産物は「多」(無数の二分木)であり、しかも各産物は文法を自己の構造として体現している。
西田はさらに「作られたものから作るものへ」という動的方向性を強調するが[11]、これはEML式の評価($\mathrm{eval}$)という「作られた式から数値を作る」演算に対応する。式は静的な木構造(作られたもの)であるが、評価によって数学的対象(作るもの)を生成する。
5.4 Girardのパラドックスとラッセルのパラドックスの統一的把握
本稿の分析を通じて、型論的矛盾と集合論的矛盾の同一構造が浮かび上がる:
| 体系 | パラドックス | 問題の核心 | 解決策 |
|---|---|---|---|
| ZFC集合論 | Russellのパラドックス | $\{x \mid x \notin x\}$ の集合化 | 真クラス(NBG/MK) |
| MLTT | Girardのパラドックス | $\mathsf{Type} : \mathsf{Type}$ | 宇宙階層($\mathcal{U}_i : \mathcal{U}_{i+1}$) |
| EML体系 | $\mathcal{U}_{\mathrm{EML}}$ の集合化 | 全生成物の自己包含 | 真クラスとしての $\mathcal{U}_{\mathrm{EML}}$ |
| 易 | (哲学的対応) | 太極が万物を含むが万物の一つではない | 無極による超越 |
| 西田哲学 | (哲学的対応) | 世界は個物を含むが個物ではない | 場所(絶対無) |
表2:各体系における「全体の自己包含問題」と解決策
三つの数学的・論理的解決策(真クラス、宇宙階層、真クラスとしての $\mathcal{U}_{\mathrm{EML}}$)は、形式的には同一の原理——「全体は自分自身の要素にはなれない」——を異なる枠組みで実装したものである。そして「無極」と「絶対無」はこの原理の哲学的直観として、東洋思想において独立に発見されていたと解釈できる。
§6 考察と残された問題
6.1 Odrzywołek論文へのプラスアルファとしての位置づけ
Odrzywołek(2026)の論文は構成的数学の立場から、個々の初等関数の表現可能性を論じる。本稿が追加する層は二つある:
存在論的層:「EMLで生成可能な全対象の総体 $\mathcal{U}_{\mathrm{EML}}$ の存在論的地位は何か」という問い。本稿はこれを真クラスとして定位し、Odrzywołekの完全性定理(各個別関数の表現可能性)と矛盾しない形で「全体の不可対象化」を定式化した。
型論的層:EML文法をMLTTの帰納型 $\mathrm{Expr} : \mathcal{U}_0$ として再定式化することで、Agda等の証明支援系における形式検証の可能性を開く。定理3.2は原理的にAgdaで形式証明可能な命題として再定式化できる。
6.2 今後の課題
課題1(圏論的定式化):表1の四層対応を圏論的に精確化すること。具体的には、EML式の圏・MLTT型の圏・易の変化の圏の間に関手(functor)を構成し、「構造的同型」を射の存在として証明することが目標となる。
課題2(形式検証):定義3.1と定理3.2をAgdaまたはCoqで実装し、完全性定理の一部を機械的に検証すること。これによりEML体系の数学的基礎が型論的に確立される。
課題3(西田論理の形式化):西田の「場所の論理」を依存型理論の枠組みで再構成する試みは萌芽的段階にある。「場所」を文脈(context) $\Gamma$ として、「絶対矛盾的自己同一」を $\Gamma$ の自己適用($\Gamma \vdash \Gamma\ \mathrm{type}$)として解釈する方向が考えられるが、これはGirardのパラドックスと同型の問題を再び招くことになる。この循環をいかに型論的に解消するかが核心的課題である。
課題4(三項EMLの研究):Odrzywołekは論文末尾で「定数を必要としない三項EML変種」の存在を示唆している[1]。この三項演算子は、易の三爻(三本の爻が八卦を構成する)との対応において、本稿の図式をより精密化する可能性がある。
6.3 方法論的反省
本稿は異なる文化的・歴史的文脈で生まれた概念体系の間に構造的対応を見出すことを試みた。この試みの正当性と限界について明示的に述べておく必要がある。
正当性:表1の各対応は、各体系の内部における形式的定義に基づく。「無極=真クラス」は比喩ではなく、「両者が共有する形式的性格(集合でない全体・操作の対象にならない・しかし全対象を含む場所)」に基づく構造的対応として提示されている。
限界:西田哲学や易の体系は本来、形式的定義ではなく洞察的・実践的文脈で理解されるものである。本稿の形式化は、これらの体系の一側面を数学的に照らすものであり、それらの全体を捕捉するものではない。形式化によって失われるものへの感受性を保持することもまた、誠実な学術的態度として求められる。
§7 結論
本稿は以下の三点を示した。
第一に、EML体系をMLTT帰納型 $\mathrm{Expr} : \mathcal{U}_0$ として再定式化することで、Odrzywołekの構成的完全性定理を型論的枠組みで表現できる。定数 $1$ は帰納型の基底ケース($\mathrm{one} : \mathrm{Expr}$)として、$\mathrm{eml}$ は再帰的構成子として自然に解釈される。
第二に、「EMLで意味論的に到達可能な全対象の総体 $\mathcal{U}_{\mathrm{EML}}$」は集合ではなく真クラスであり、これは周敦頤の「無極」の数学的定式化として機能する。この定位はOdrzywołekの完全性定理(各個別関数の表現可能性)と矛盾せず、むしろ体系の存在論的基盤を明確化する。
第三に、無極(真クラス)・太極($\mathrm{eml}$ 演算子)・陰陽($\exp/-\ln$ 双対)・万物($\mathrm{Expr}$ の項)という四層図式が、MLTT宇宙階層・西田の「絶対矛盾的自己同一」・易の陰陽八卦生成論において構造的に共鳴する。この収束は、生成的構造の形式的普遍性——最小生成元、非対称双対性、再帰的展開、全体の不可対象化——が、数学的・哲学的・東洋宇宙論的文脈を横断して独立に発見されてきたことを示唆する。
これらの知見は、Odrzywołek論文が開いた地平に「存在論的層」と「哲学的連関」という二つの次元を付加するものである。
§ 参考文献
-
“All elementary functions from a single binary operator.”
arXiv:2603.21852 [cs.SC], 2026年3月(改訂版2026年4月).
doi:10.48550/arXiv.2603.21852 -
“An Intuitionistic Theory of Types: Predicative Part.”
in Logic Colloquium ’73, H.E. Rose and J.C. Shepherdson (eds.),
North-Holland, pp. 73–118, 1975. -
“Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur.”
Thèse d’État, Université Paris VII, 1972. -
“Intuitionistic Type Theory.”
Notes by Giovanni Sambin of a series of lectures given in Padova, June 1980.
Bibliopolis, Naples, 1984. -
“On Universes in Type Theory.”
in Twenty-Five Years of Constructive Type Theory, G. Sambin and J.M. Smith (eds.),
Oxford University Press, pp. 191–204, 1998. -
“Homotopy Type Theory: Univalent Foundations of Mathematics.”
Institute for Advanced Study, 2013.
Available: https://homotopytypetheory.org/book/ -
“Programming in Martin-Löf’s Type Theory: An Introduction.”
Oxford University Press, 1990. -
『太極図説』(Tàijí Túshuō), 11世紀.
朱熹注(南宋). 収録:『朱文公文集』. -
「場所」, 『働くものから見るものへ』所収,
岩波書店, 1927.
西田幾多郎全集 第4巻. -
『通書』(Tōngshū), 11世紀.
「動而生陽、静而生陰」の出典. -
「絶対矛盾的自己同一」, 1939年.
岩波書店. 西田幾多郎全集 第9巻, pp. 147–222.
青空文庫:https://www.aozora.gr.jp/cards/000182/card1755.html -
「場所的論理と宗教的世界観」, 1945年.
岩波書店. 西田幾多郎全集 第11巻. -
“A Set of Five Independent Postulates for Boolean Algebras, with Application to Logical Constants.”
Transactions of the American Mathematical Society, 14(4), pp. 481–488, 1913. -
“A Finite Axiomatization of Inductive-Recursive Definitions.”
in Typed Lambda Calculi and Applications, TLCA 1999,
Lecture Notes in Computer Science, vol. 1581, Springer, pp. 129–146, 1999. -
『周易注』, 三国時代(3世紀).
「易窮則變、變則通、通則久」.