項 (論理学)

数理論理学における項（こう、テンプレート:Lang-en-short）とは、式または論理式のなかで数学的対象を表す、依存的／束縛された記号の配列である。特に項は論理式の構成要素として現れる。これは自然言語において名詞句が対象を、文全体が事実を指すことと類似している。

一階の項は、定数記号、変数記号、関数記号から再帰的に構成される。適切な数の項に述語記号を適用して形成される式は原子論理式と呼ばれ、解釈が与えられれば二値論理において真または偽の値をとる。たとえば テンプレート:Tmath は定数 1、変数 テンプレート:Mvar、および二項関数記号 テンプレート:Tmath と テンプレート:Tmath から構築された項であり、原子論理式 テンプレート:Tmath の一部となる。この原子論理式は テンプレート:Mvar の各実数値について真の値をとる。

論理学以外にも、項は普遍代数学やテンプレート:仮リンクにおいて重要な役割を果たす。

定義

左から右へ: 項 (n⋅(n+1))/2 および n⋅((n+1)/2) の木構造

変数記号の集合 V、定数記号の集合 C、および各自然数 n ≥ 1 に対する n 項関数記号（演算記号ともいう）の集合 F_n が与えられたとき、（無ソートの一階の）項の集合 T は次の性質を満たす最小の集合として再帰的に定義される。

• すべての変数記号は項である: テンプレート:Math、
• すべての定数記号は項である: テンプレート:Math、
• 任意の n 個の項 t₁,...,t_n と、任意の n 項関数記号 テンプレート:Math から、より大きな項 f(t₁, ..., t_n) を構築できる。

直観的な擬テンプレート:仮リンク記法を用いれば、これは以下のように書かれることもある。

t ::= x | c | f(t₁, ..., t_n)

項言語のシグネチャは、どの関数記号集合 F_n が空でないかを記述する。よく知られた例として単項関数記号 テンプレート:Math や、二項関数記号 テンプレート:Math などがある。三項演算やそれ以上のアリティの関数も可能だが、実際にはあまり見られない。多くの著者は定数記号を 0 項関数記号 F₀ と見なすため、それらに対する特別な構文クラスを必要としない。

項は議論領域の数学的対象を表す。定数 c はその領域の名前付きの対象を表し、変数 x はその領域の対象の範囲を動き、n 項関数 f は対象の n 組を対象に写像する。たとえば テンプレート:Math を変数記号、テンプレート:Math を定数記号、テンプレート:Math を二項関数記号とすると、第 1、第 2、第 3 の項構築規則によりそれぞれ テンプレート:Math が成り立ち、（したがって）テンプレート:Math となる。後者の項は通常、中置記法と、より一般的な演算記号 + を用いて便宜的に n+1 と書かれる。

項の構造と表現

本来、論理学者は項をある構築規則に従う文字列として定義していた。しかしながら、計算機科学において木という概念が普及するにつれ、項を木として考える方が便利であることが明らかになった。たとえば「テンプレート:Math」、「テンプレート:Math」、「$\frac{n(n+1)}{2}$」など、いくつかの異なる文字列は同じ項を表し、同じ木、すなわち上図の左の木に対応する。項の木構造をその紙上のグラフィカルな表現から切り離せば、括弧（表現のみで構造にはない）や不可視の乗算演算子（構造にはあるが表現にはない）を扱うことも容易となる。

構造的等価

2 つの項が構造的、字義的、構文的に等しいとは、それらが同じ木に対応することをいう。たとえば上図の左と右の木は、有理数演算では常に同じ値をとるため「意味的に等しい」と見なされうるものの、構造的には等しくない項である。構造的等価は記号の意味に関する知識なしで検証できるが、意味的等価はそうではない。もし関数 / が有理数除算ではなく切り捨て整数除算として解釈された場合、n=2 のとき左と右の項はそれぞれ 3 と 2 の値をとる。構造的に等しい項は変数名が一致していなければならない。

これに対して、項 t が項 u の名前替えまたは変異体と呼ばれるのは、後者が前者のすべての変数を一貫して名前替えして得られたとき、すなわちあるテンプレート:仮リンク σ について u = tσ となるときである。この場合、名前替え代入 σ は逆 σ⁻¹ を持ち t = uσ⁻¹ となるから、u もまた t の名前替えである。両項はまた名前替えを法として等しいともいわれる。多くの文脈において項の中の具体的な変数名は問題とならない。たとえば加法の可換性公理は x+y=y+x とも a+b=b+a とも述べることができる。こうした場合、論理式全体は名前替えしてよいが、任意の部分項は普通は名前替えできない。たとえば x+y=b+a は可換性公理の妥当な形式ではない。

接地項と線型項

項 t の変数の集合は vars(t) と表記される。変数を全く含まない項は接地項と呼ばれ、変数の複数出現を含まない項は線型項と呼ばれる。たとえば 2+2 は接地項であり、したがって線型項でもある。x⋅(n+1) は線型項、n⋅(n+1) は非線型項である。これらの性質は、たとえば項書き換えにおいて重要である。

関数記号に対するシグネチャが与えられたとき、すべての項の集合は自由項代数を成す。すべての接地項の集合は始項代数を成す。

定数の個数を f₀、i 項関数記号の個数を f_i と略記すると、高さ h までの相異なる接地項の個数 θ_h は次の再帰式で計算できる。

• θ₀ = f₀。高さ 0 の接地項は定数しかありえないから、
• ${\theta }_{h+1}=\sum _{i=0}^{\mathrm{\infty }}{f}_i\cdot {\theta }_h^i$。高さ h+1 までの接地項は、i 項の根関数記号を用いて高さ h までの任意の i 個の接地項を合成することで得られるから。定数と関数記号の個数が有限であればこの和は有限値をとり、通常はそうである。

項からの論理式の構築

各自然数 n ≥ 1 に対する n 項関係記号の集合 R_n が与えられたとき、（無ソートの一階の）原子論理式は n 項関係記号を n 個の項に適用することで得られる。関数記号と同様、関係記号の集合 R_n は通常、小さい n に対してのみ空でない。数理論理学において、より複雑な論理式は原子論理式から論理結合子と量化子を用いて構築される。たとえば テンプレート:Mathbb を実数の集合とすると、テンプレート:Math は複素数の代数において真の値をとる数学的論理式である。原子論理式は、それが完全に接地項から構築されていれば接地であるといい、関数記号と述語記号の与えられた集合から構成しうるすべての接地原子論理式は、これらの記号集合に対するヘルブラン基底を成す。

項に対する演算

黒の例項 $\frac{a\ast ((a+1)\ast (a+2))}{1\ast (2\ast 3)}$ の木構造。青の redex は テンプレート:Tmath

• 項は木階層の構造をもつため、その各ノードには位置または経路、すなわちそのノードの階層内の位置を示す自然数の列を割り当てることができる。空列（通常 ε と記される）は根ノードに割り当てられる。図中では黒の項内の位置列が赤で示されている。
• 項 t の各位置 p には一意な部分項が始まり、通常 テンプレート:Math と表記される。たとえば図の黒の項の位置 122 では、部分項 a+2 がその根に位置する。「の部分項である」という関係は項の集合上の半順序である。各項は自明にそれ自身の部分項であるから、反射的である。
• 項 t の位置 p にある部分項を新しい項 u に置き換えることで得られる項は通常 テンプレート:Math と表記される。項 テンプレート:Math はまた、項 u と項に似た対象 テンプレート:Math との一般化された結合の結果としても見ることができる。後者は文脈、あるいは（「.」で示される）穴を持つ項と呼ばれ、その位置が p であり、そこに u が埋め込まれる。たとえば t を図の黒の項とすると、テンプレート:Math は項 $\frac{a\ast (b+1)}{1\ast (2\ast 3)}$ となる。後者の項は、項 テンプレート:Math を文脈 $\frac{a\ast (.)}{1\ast (2\ast 3)}$ に埋め込むことによっても得られる。非公式にいえば、具体化と埋め込みの演算は互いに逆である。前者は関数記号を項の下部に付加するのに対し、後者は上部に付加する。テンプレート:仮リンクは、項と両側からの付加のあらゆる結果とを関連づける。
• 項の各ノードには、その深さ（一部の著者では高さとも呼ばれる）、すなわち根からの距離（辺の個数）を割り当てることができる。この場合、ノードの深さは常にその位置列の長さに等しい。図では、黒の項における深さレベルが緑で示されている。
• 項のサイズは、通常そのノード数、あるいは同等に、括弧を除く記号数として数えた項の書かれた表現の長さを指す。図の黒と青の項はそれぞれサイズ 15 と 5 である。
• 項 u が項 t にマッチするとは、u の代入インスタンスが t の部分項と構造的に等しいこと、つまり形式的には、t の位置 p とある代入 σ について テンプレート:Math となることをいう。この場合、u、t、σ はそれぞれパターン項、対象項、マッチング代入と呼ばれる。図では、青のパターン項 テンプレート:Tmath が黒の対象項の位置 1 においてマッチしており、マッチング代入 テンプレート:Math が黒の代入項のすぐ左にある青の変数で示されている。直観的には、パターンはその変数を除いて対象項に含まれていなければならず、パターンで変数が複数回出現する場合、対象項の対応する各位置に同じ部分項が必要となる。
• 項の単一化
• 項書き換え

関連概念

ソート付き項

テンプレート:Main 議論領域が本質的に異なる種類の要素を含む場合、すべての項の集合をそれに応じて分割すると便利である。この目的のため、各変数と各定数記号にソート（型とも呼ばれる）が割り当てられ、各関数記号にドメインソートおよびレンジソートの宣言が割り当てられる。ソート付き項 f(t₁,...,t_n) は、テンプレート:Mvar 番目の部分項のソートが f の宣言された テンプレート:Mvar 番目のドメインソートと一致する場合にのみ、ソート付き部分項 t₁,...,t_n から構成できる。このような項は適切にソート付けされているとも呼ばれ、それ以外の項（すなわち無ソートの規則のみに従う項）は不適切にソート付けされていると呼ばれる。

たとえばベクトル空間には、それに関連するスカラー数の体が付随している。W と N をそれぞれベクトルと数のソートとし、V_W と V_N をそれぞれベクトル変数と数変数の集合、C_W と C_N をそれぞれベクトル定数と数定数の集合とする。すると、たとえば $\overrightarrow{0}\in C_W$ および テンプレート:Math となり、ベクトルの加算、スカラー乗算、内積はそれぞれ テンプレート:Tmath および テンプレート:Tmath と宣言される。変数記号 $\overrightarrow{v},\overrightarrow{w}\in V_W$ と テンプレート:Math を仮定すると、項 $⟨(\overrightarrow{v}+\overrightarrow{0})\ast a,\overrightarrow{w}\ast b⟩$ は適切にソート付けされているが、$\overrightarrow{v}+a$ はそうではない（+ は第 2 引数としてソート N の項を受け付けないため）。$a\ast \overrightarrow{v}$ を適切にソート付けされた項にするためには、追加の宣言 テンプレート:Tmath が必要である。複数の宣言を持つ関数記号はオーバーロードされていると呼ばれる。

詳細（ここで説明した多ソートフレームワークの拡張を含む）については多ソート論理を参照。

ラムダ項

束縛変数を持つ項

記法例	束縛 変数	自由 変数	ラムダ項として 書き表すと
テンプレート:Math	n	x	limit(λn. div(x,n))
$\sum _{i=1}^n{i}^2$	i	n	sum(1,n,λi. power(i,2))
${\int }_a^b\sin (k\cdot t)dt$	t	a, b, k	integral(a,b,λt. sin(k⋅t))

動機

表に示すような数学的記法は、上で定義された一階の項の枠組みに収まらない。なぜならそれらはすべて、記法のスコープ外に現れることのできない独自の局所または束縛変数を導入するからである。たとえば $t\cdot {\int }_a^b\sin (k\cdot t)dt$ は意味をなさない。これに対して、自由変数と呼ばれる他の変数は通常の一階の項変数のように振る舞う。たとえば $k\cdot {\int }_a^b\sin (k\cdot t)dt$ は意味をなす。

これらの演算子はすべて、値項ではなく関数を引数の一つとしてとるものと見なすことができる。たとえば lim 演算子は数列、すなわち正整数から（たとえば）実数への写像に適用される。別の例として、表の第 2 の例 Σ を実装する C 言語の関数は関数ポインタ引数を持つことになる（下記のボックス参照）。

ラムダ項は、lim、Σ、∫ などに引数として供給される無名関数を表すために用いることができる。

たとえば下記の C プログラムの関数 square は、ラムダ項 λi. i² として無名で書くことができる。一般の総和演算子 Σ は、下限値、上限値、および総和されるべき関数をとる三項関数記号と見なせる。この最後の引数の存在ゆえに、Σ 演算子は二階の関数記号と呼ばれる。他の例として、ラムダ項 λn. x/n は、1, 2, 3, ... をそれぞれ x/1, x/2, x/3, ... に写像する関数、すなわち数列 (x/1, x/2, x/3, ...) を表す。lim 演算子はそのような数列をとり、（定義される場合の）その極限を返す。

表の一番右の列は、各数学記法例をラムダ項でどのように表現できるかを示し、また一般的な中置演算子を前置形に変換している。

// implements general sum operator
int sum(int lwb, int upb, int fct(int)) {
    int res = 0;
    for (int i=lwb; i<=upb; ++i)
        res += fct(i);
    return res;
}

// implements anonymous function (lambda i. i*i); however, C requires a name for it
int square(int i) { return i*i; }


#include <stdio.h>
int main(void) {
    int n;
    scanf(" %d",&n);
    printf("%d\n", sum(1, n, square));        // applies sum operator to sum up squares
    return 0;
}

定義

テンプレート:節スタブ 変数記号の集合 V が与えられたとき、ラムダ項の集合は次のように再帰的に定義される。

• すべての変数記号 x∈V はラムダ項である。
• x∈V が変数記号で t がラムダ項ならば、λx.t もラムダ項である（抽象化）。
• t₁ と t₂ がラムダ項ならば、( t₁ t₂ ) もラムダ項である（適用）。

上の動機の例では div、power などの定数も用いたが、これらは純粋なラムダ計算では認められない。

直観的には、抽象化 λx.t は x が与えられたとき t を返す単項関数を表し、適用 ( t₁ t₂ ) は関数 t₁ を入力 t₂ で呼び出した結果を表す。たとえば抽象化 λx.x は恒等関数を表し、λx.y は常に y を返す定数関数を表す。ラムダ項 λx.(x x) は関数 x をとり、x 自身に x を適用した結果を返す。

関連項目

• 方程式
• 数式

参考文献

• テンプレート:Cite book