$\lambda+$ 項の値の上限について 東北大学工学研究科 竹内 泉 (Takeuti, Izumi)
1
$\lambda+$ 項 $\lambda+$ 項は、 型付 $\lambda$ 計算の部分体系であ り、 型付 $\lambda$ 項の $\beta$ 変 換列の長さの上限を与える際に有用である。 [参考文献 1] $\lambda+$ 項は型付 $\lambda$ 項に次のような制限を加えたものとして定 義される。.
原子型は $\omega$ のみ。.
型の構成子は $\supset$ のみ。.
原子定項は $0\in\omega$ 、 $s\in\omega\supset\omega$ 、 $+\in\omega\supset\omega\supset\omega$ のみ。.
変数は各型に対し十分に多くある。.
計算規則は、 $a$ 同値、 $\beta$ 同値、 $\eta$ 同値に加えて、 次のものがある。
$+0t=+t0=t$
$+(st)u=+t(su)=s(+tu)$
$+tu=+ut$
$+(+tu)v=+t(+uv)$ $\bullet$ シュビ ッ テンベルクの上界 型付 $\lambda$ 項の正規化可能性 [参考文献 3] により、 型が $\omega$ である $\lambda+$ 項はある数を表す。 項の構文上の複雑さから項の値に上界を与えることは重要 である。 シュビッテンベルクはこの問題に於いてある上界を 与えた。 シュビ ッ テンベルクの上界を説明する為に、 クヌスの記号 $\uparrow\uparrow$ を紹介する $0$ これは二項演算であって、 次のように定義 する。 $x\uparrow$ $\uparrow 0$ : $=1$
$x\uparrow$ $\uparrow n+1$
:
$=x^{X}\uparrow\uparrow n$普通の記号に依れば
$x\uparrow\uparrow n=x^{x}$
の
}
$n$ ケ$n$ を固定して $xarrow x+2\uparrow\uparrow n$ という函数を考えると、 これ
は初等函数であ り、 函数列 $\{xarrow x+2\uparrow\uparrow n\}_{n=0,1},\cdots$ は初等函数
の中で共終である。 シュビッテンベルクは型が $\omega$ である任意の閉 $\lambda+$ 項 $t$ に対 して、 項の値を $\mathbb{I}tJ$ 、 項の長さを $l$ 、 現れる変数の階級の最 高のものを $q$ で表すと、
[
$t$I
は $l+2\uparrow\uparrow 2q$ 程度で圧さえられ ることを示した。 [参考文献 2] ここでは、 $3l\uparrow\uparrow q+2$ で圧さえられることを示す。2
項と型$\bullet$ 長さ、 階級、 位数
型と項に対して、 長さ $length[]$ 、 階級
rank
$[]$ 、 位数 $\circ rder[]$を定義する。
$length[\omega]$ $:=1$
$length[T\supset U]$
$:=length[T]+length[U]$
X
が型 $T$ の原子項な らば$length[X ]:=length[T]$
$length[\lambda x.X]$ $:=length[X]$
$length$
[
XY]
$:=length[X]+length[Y]$
$rank[\omega]$ $:=0$
$rank[T\supset U]$ $:= \max\{rank[T]+1, rank[U]\}$ $x\in T$ ならば
$rank[X|:=rank[T]$
$order[\omega]$ $:=0$
$order[T\supset U]$
$:=order[U]+1$
$X\in T$
Zit
ら $a^{\backslash }$ $order[X]$$:=\circ rder[T]$ $\bullet$ 意味論 型が $\omega$ である閉項は整数を表す。 数 $n$ を表す項 $s(s(\cdots s(s0)\cdots))$ $-$ $s$ が $n$ ケ を $\overline{n}$ と書く。 そうすると、 型 $\omega$ の閉項 $t$ に対してある数 $n$ が あって 、 $t=\overline{n}$ となる。 この $n$ を
[
$t$I
と書く。 すなわち $t=\overline{n}$ $\Leftrightarrow$$n=[t$
I
$\bullet$ 整数の表す型整数に依ってある一連の型を表す。 $0$ : $=\omega$
$n+1$ :
$=n\supset n$ これは単なる略記であって、 数と型を同じと見倣すものでは ない。3
順序 同じ型をした閉項の問に部分順序関係を定義する。 定義は、 型の複雑さ に関する帰納法で行なう。型 $\omega$ に対しては、
X
$\leqq Y\Leftrightarrow[xI\leqq[YJ$X, $Y\in\prime r\supset u$ に対しては、
X
$\leqq Y$ $\Leftrightarrow$ 型 $T$ の任意の閉項 $Z$ に対し、X
$Z\leqq YZ$ 一般の項に対しても、 同じ型の項の問に同様の部分順序を 定義する。 今度は、 『 \leqq 』 の両辺に含まれる自由変数の数の 帰納法に依り行なう。 $X$ , $Y$ は同じ型の項で、 $x$ はどちらかに自由変数として含まれる変数である時、 $X\leqq Y$ $\Leftrightarrow$ $\lambda x.X\leqq\lambda x.Y$
この定義は次を意味する。 ここで $\ddot{u}$ は
X
、 $Y$ に含まれる自 由変数を全て列べたものである。X
$\leqq Y$ $\Leftrightarrow$ $uarrow$ と型が適合する任意の閉項の列 $\ddot{Z}$ に対し、 $X[\vec{Z}/uarrow]\leqq Y[\vec{Z}/uarrow]$この時 $X[\dot{\vec{Z}}/uarrow]$ と $Y[\dot{\tilde{Z}}/\overline{u}’]$ は閉項になる。 次の命題が成り立つ。 項 $X\in T\supset U$ 、 $Y,Z\in T$ に対して $Y\leqq Z$ $\Rightarrow$ $XY\leqq XZ$
項 X,Y $\in T\supset U$
、 $Z\in T$ に対して
X
$\leqq Y$$\Rightarrow$
XZ
$\leqq$YZ
変数 $x$ と項 X,$Y$ に対して $X\leqq Y$ $\Rightarrow$ $\lambda x.X\leqq\lambda x.Y$
4
定項 $\bullet|$ 、 $0$ 、 $+$ 型 $T$ に対して $|^{T\supset T}$ $:=\lambda x^{T}.x^{T}$ 型 $T$ に対して$O^{T}$は $O^{\omega}$ $:=0$$O^{T\supset U}$ $:=\lambda x^{T}.O^{U}$
型 $T$ に対して$+\tau\in T\supset T\supset T$ は
$+_{\omega}$ $:=+$ $+\tau\supset U$ $:=\lambda_{X}+(xz)(yz)$ 以降、 $+$ はある型 $T$ に対する $+\tau$を表し、 必ずしも $+_{\omega}$ を表さ ない。 $\bullet P$ 、 $Q$ 、 $R$ 、 $M$ 整数 $n\geqq 1$ に対して
$P_{n}$ $:=\lambda ux_{n-2}\cdots x_{0}y_{n-2}\cdots y_{0}.u(+x_{n-2}y_{n-2})\cdots(+x_{0}y_{0})$
次が成り立つ。
$P_{1}=|$
整数 $n\geqq 2$ に対して
$Q^{n}$ $:=\lambda uvx_{n-3}\cdots x_{0}$
.
$u(P_{n-1}vx_{n-3}\cdots x_{0})$$(P_{n-2}(vx_{n-3})x_{n-4}\cdots x_{0})$ $(P_{2}(vx_{n-3}\cdots x_{1})x_{0})$ $(vx_{n-3}\cdots x_{0})$ 次が成り立つ。 $Q^{2}=|$ 整数 $n\geqq 2$ に対して $R^{2}$ $:=|$
$R^{n}:=\lambda uvw.Q^{n-1}(uv)(uvw)$ $-$ 但し $n\geqq 3$
整数 $n\geqq 1$ 及び $i\geqq 0$ に対して
$M_{0}^{1}$ $:=s$
$n\geqq 2$ ならば $M_{0}^{n}$ $:=+|(\lambda u.M_{0}^{n-1})$
$i\geqq 1$ ならば $M_{i}^{n}$ $:=(+|R^{n+1})M_{i-1}^{n}$
$+$ 、 $P$ の下付添字と
1
、 $0$ 、 $Q$ 、 $R$ 、 $M$ の上付添字は型 を表す。 型の推定が容易な場合には、 型を表す添字は省略し て書かない。$\bullet F$ 、 $G$ 階級 $n$ の型 $T$ に対して、 順序準同型写像$F$ :(型 $T$ の項) $arrow$ (型 $n$ の項) と $G$
:
(型 $n$ の項) $arrow$ (型 $T$ の項) を導入する。 項$F_{T}$ と $G_{T}$ は $F$ と $G$ の表現である。 項によって表現される写像 が準同型になることは明かである。型 $T$ 及び整数 $n\geqq rank[T]$ に対して $F^{T\supset n}$
及び $G^{n\supset T}$
を定義する。
これは $T$ の帰納法で行なう。
まず $T=\omega$ の場合、 $F^{\omega\supset n}:=\lambda vx_{n-1}\cdots x_{0}.v$
$G^{n\supset\omega}:=\lambda u.uO^{n-1}$
...
$O^{0}$$T\neq\omega$ の場合は、 $T$ を
$T=T_{1}\supset T_{2}\supset\cdots T_{h}\supset\omega$
と表す。 $h=\circ rder[T]$ である。 この$T_{1}\cdots T_{h}$ を階級に依って分類
する。
階級 $0$ $-$
$T_{j_{0,1}}$
. .
.
$T_{j_{0,h_{0}}}$階級 1 $-$ $T_{j_{1,1}}$
.
.
.
$T_{j_{1,h_{1}}}$$\mathbb{P}\in:\# Rn-1$ – $T\cdot$ $\cdots T$ .
$\gamma_{n-1,1}$ $g_{n-1,h_{n-1}}$
$h_{0}+h_{1}+\cdots h_{n-1}=h$ であり、 $j_{k,l}$ は1 から $h$ までを動く。 $h_{0},$ $h_{1}\cdots h_{n-1}$ の中には $0$ があるかも知れない。 以降は $T_{j_{k,l}}$ を
乃
,l
と書く。 $T_{k,1}\cdots T_{k,h_{k}}$ の中には重複して現れる ものがあるさて、 変数 $x_{1}^{T_{1}}\cdots x_{h}^{T_{h}}$ を考える。 $T_{j}$ と $T_{k,l}$ のように、 $x_{j_{k,l}}$ を $x_{k,l}$ と書く。 この時、
$G^{n\supset T}$ を
$G^{n\supset T}:=\lambda ux_{1}$
$x_{h}.uV_{n-1,\backslash }\cdots V_{0}$
と定め る 。 ここで $V_{n-1}$ $v_{0}$ は
$V_{k}:=+(F^{T_{k,1}\supset k_{X_{k,1}}})$
$(+(F^{T_{k,2}\supset k_{X_{k,2}}})$
$($ ... $+(F^{T_{k,h_{k}-1}\supset k_{X_{k,h_{k}-1}}})$
$(F^{T_{k,h_{k}}\supset k_{\cross k,h_{k}}})$
...
))
$-$ $h_{k}\geqq 2$ の時V
$k;=F^{T_{k,1}\supset k_{X_{k,1}}}$ $-$ $h_{k}=1$ の$\#_{f}^{\pm}\backslash$$V_{k}:=0^{k}$ $-h_{k}=0$ の時
を表す。
$F^{T\supset n}$
は
$F^{T\supset n}:=\lambda vx_{n-1}$ $x_{0}.v(G^{rank[T_{1}]\supset T_{1}}x_{rank[T_{1}]})\cdots(G^{rank[T_{h}]\supset T_{h}}x_{rank[T_{h}]})$
と定める。
単に型 $T$ のみを指定した時には、
$F_{T}:=F^{T\supset rank[T]}$ , $G_{T}:=G^{rank[T]\supset T}$
を表す。
次が成り立つ。
$G_{T}(F_{T}x)$ $\geqq x$
$n\geqq rank[T]$ ならば、 $n$ に依らず
5
補題補題 1 $\lambda u.F_{T}(G_{T}u)\leqq M_{length[T]-1}$
補題2 $\lambda v.QM_{i}^{n}(M_{j}^{n}v)\leqq M_{i+j+2}^{n}$
補題 3 $M_{i}^{n+1}0^{n}\leqq M_{2-3}^{n_{i+3}}$ 但し $n\geqq 1$
6
定理閉項
X
の長さ $l$=length[X]
、 階級 $r$
=rank[
温]
、X
の中にある変数と原子定項の中で階級が一番高いものの階級が $q$ である
I寺、 $FX\leqq M_{3l-3}^{q+1}O^{q}\cdots O^{r}$
7
系 閉項X
$\in\omega$ に対し、 $length[X]=l$ 、 $X$ の中にある原子項の中 で階級が一番高いものの階級を $q$ と書く時、 $[XJ\leqq 2_{q+1}^{3l}-3$ 但しここで $2_{0}^{n}=n,$ $2_{i+1}^{n}=2^{2_{i}^{n}}$8
結論 定理により、 項の列 $\{M_{i}^{n}\}_{i=0,1},\cdots$ は型 $n$ の閉項の中で共終で ある。 また$F(Gx)\geqq x$ であることから、 列 $\{G_{T}M_{i}\}_{i=0,1},\cdots$ もまた 型 $T$ の閉項の中で共終であることが示される。$\uparrow\uparrow q+2$ という評価が得られる。 この不等式に於いて、 $\uparrow\uparrow$
の第二引数に於ける $q$ の一次の係数が
1
より小さ くならないことは既に知られている。 [参考文献 2] その意味で、 この
不等式は最良の評価である。
9
参考文献[1] Gandy,
R.
$0$.: Proof
of
strongnormalization.
To
H.B.
Curry
Essays
$i_{7}\iota$Combinatory Logic, Lambda
Calculus
and
Formalism.
1980
[2]
Shwichtenberg, H.
:
Complexity of normalization
in
the
pure
typed lambda
-ca[culus.
