用語（ロジック）

数理論理学では、用語は数学的な対象を表し、式は数学的な事実を表します。特に、用語は式の構成要素として現れます。これは、名詞句が対象を表し、文全体が事実を表す 自然言語に似ています。

一階項は、定数記号、変数、関数記号から再帰的に構築されます。述語記号を適切な数の項に適用して形成される式は原子式と呼ばれ、解釈が与えられた場合、二価論理で真または偽に評価されます。たとえば、⁠ ⁠は、定数 1、変数x、および二項関数記号⁠ ⁠と⁠ ⁠から構築された項であり、 xの実数値ごとに真に評価される原子式⁠ ⁠の一部です。 ${\displaystyle (x+1)*(x+1)}$${\displaystyle +}$${\displaystyle *}$${\displaystyle (x+1)*(x+1)\geq 0}$

論理学の他にも、項は普遍代数や書き換えシステムにおいて重要な役割を果たします。

変数記号の集合V 、定数記号の集合C 、およびn項関数記号（演算子記号とも呼ばれる）の集合Fn （各自然数n≥1 ）が与えられたとき、（_ソートされていない1次）項の集合Tは、次の特性を持つ最小の集合として再帰的に定義される： ^[1]

• すべての変数記号は項である: V ⊆ T、
• すべての定数記号は項である: C ⊆ T、
• すべてのn項t ₁ ,..., t _nとすべてのn項関数記号f ∈ F _nから、より大きな項f ( t ₁ ,..., t _n ) を構築できます。

直感的な疑似文法表記を使用すると、次のように記述されることもあります。

t  ::= x | c | f ( t ₁ , ..., t _n ) です。

用語言語のシグネチャは、どの関数記号セット F n が存在するかを表します。よく知ら_れている例としては、単項関数記号sin、cos ∈ F ₁、および二項関数記号 +、−、⋅、/ ∈ F ₂があります。三項演算やより高次の関数も可能ですが、実際には一般的ではありません。多くの著者は、定数記号を 0 項関数記号F ₀と見なしており、そのため特別な構文クラスは不要であると考えています。

項は、論議領域の数学的オブジェクトを表します。定数c はその領域の名前付きオブジェクトを表し、変数x はその領域のオブジェクトの範囲を表し、n項関数f はn組のオブジェクトをオブジェクトにマップします。たとえば、n ∈ Vが変数記号、 1 ∈ Cが定数記号、add ∈ F _{2 が}2項関数記号である場合、第1、第2、および第3項構築規則により、それぞれn ∈ T、 1 ∈ T、および (したがって) add ( n、 1) ∈ Tとなります。後者の項は通常、便宜上、 中置記法とより一般的な演算子記号 + を使用してn +1と記述されます。

もともと、論理学者は項を特定の構築規則に従った文字列として定義していました。 ^{[2]しかし、}ツリーの概念がコンピューターサイエンスで普及して以来、項をツリーとして考える方が便利であることがわかりました。たとえば、「( n ⋅( n +1))/2」、「(( n ⋅( n +1)))/2」、「」などのいくつかの異なる文字列は同じ項を示し、同じツリー、つまり上の図の左側のツリーに対応しています。項のツリー構造を紙の上のグラフィカル表現から切り離すと、括弧（表現のみであり、構造ではない）や目に見えない乗算演算子（構造にのみ存在し、表現には存在しない）を考慮することも簡単になります。 ${\displaystyle {\frac {n(n+1)}{2}}}$

2 つの項が同じツリーに対応する場合、それらの項は構造的、文字どおり、または構文的に等しいと言われます。たとえば、上図の左と右のツリーは構造的には等しくない項ですが、有理数演算では常に同じ値に評価されるため、 「意味的に等しい」と見なすことができます。構造的等価性は記号の意味を知らなくても確認できますが、意味的等価性は確認できません。たとえば、関数 / が有理数としてではなく、 切り捨て整数除算として解釈される場合、 n =2では左と右の項はそれぞれ 3 と 2 に評価されます。構造的に等しい項は、変数名が一致している必要があります。

対照的に、項tは項uの改名または変種と呼ばれるのは、後者が前者のすべての変数を一貫して改名した結果である場合、つまり、何らかの改名置換σ に対してu = tσである場合です。その場合、改名置換 σ には逆 σ ⁻¹があり、t = uσ ^{−1であるため、} uもtの改名です。この場合、両方の項は改名を法として等しいとも言えます。多くのコンテキストでは、項内の特定の変数名は重要ではありません。たとえば、加算の交換公理はx + y = y + xまたはa + b = b + aと表すことができます。このような場合、式全体を改名できますが、任意の部分項は通常改名できません。たとえば、x + y = b + aは交換公理の有効なバージョンではありません。^{[注 1] [注 2]}

項tの変数の集合はvars ( t )で表されます。変数を含まない項は基底項と呼ばれ、変数が複数回出現しない項は線形項と呼ばれます。たとえば、2+2 は基底項であり、したがって線形項でもあります。x ⋅( n +1) は線形項であり、n ⋅( n +1) は非線形項です。これらの特性は、たとえば項の書き換えで重要です。

関数記号のシグネチャが与えられると、すべての項の集合は自由 項代数を形成します。すべての基底項の集合は初期項代数を形成します。

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

• θ ₀ = f ₀、高さ0の基底項は定数でしかないため、
• ${\displaystyle \theta_{h+1}=\sum_{i=0}^{\infty}f_{i}\cdot \theta_{h}^{i}}$高さh +1の基底項は、高さhまでの任意のi個の基底項をi項ルート関数記号を使用して合成することで得られるためである。定数と関数記号が有限個しかない場合 (通常は有限個)、和は有限の値を持ちます。

各自然数n ≥ 1 についてn項関係記号の集合R _{n が}与えられると、 n項関係記号をn項に適用することによって (ソートされていない一階) 原子式が得られる。関数記号と同様に、関係記号集合R _nは通常、 nが小さい場合にのみ空ではない。数理論理学では、論理接続子と量指定子を使用して原子式からより複雑な式が構築される。たとえば、実数の集合∀ x : x ∈ ⇒ ( x +1)⋅( x +1) ≥ 0 を表す場合、これは複素数代数で真と評価される数式である。原子式が完全に基礎項から構築されている場合、その原子式は基礎と呼ばれます。関数記号と述語記号の特定の集合から構成可能なすべての基礎原子式は、これらの記号集合のエルブラン基底を構成します。 ${\displaystyle \mathbb {R} }$${\displaystyle \mathbb {R} }$

• 項はツリー階層構造を持つため、各ノードに位置、つまりパス、つまり階層内のノードの位置を示す自然数の文字列を割り当てることができます。一般に ε で表される空の文字列は、ルート ノードに割り当てられます。黒い項内の位置文字列は、図では赤で示されています。
• 項tの各位置pで、一意のサブ項が始まります。これは通常、t | _pで表されます。たとえば、図の黒い項の位置 122 では、サブ項a +2 にルートがあります。 「サブ項である」という関係は、項の集合の部分順序です。各項は当然それ自体のサブ項であるため、これは反射的です。
• 項t内の位置pにある部分項を新しい項uに置き換えることによって得られる項は、一般にt [ u ] _pと表記される。項t [ u ] _{p は}、項uと項のようなオブジェクトt [.]の一般化された連結から生じるものとみなすこともできる。後者はコンテキスト、または穴(「.」で示される。位置はp ) を持つ項と呼ばれ、その中にuが埋め込まれていると言われる。たとえば、図の黒い項tの場合、 t [ b +1] ₁₂の結果は項 となる。後者の項も、項b +1 をコンテキスト に埋め込むことによって生じる。非公式な意味では、インスタンス化と埋め込みの操作は互いに逆である。前者は関数記号を項の下部に追加するのに対し、後者は関数記号を上部に追加する。包含順序は、項と、両側に追加される の結果とを関連付ける。${\displaystyle {\frac {a*(b+1)}{1*(2*3)}}}$${\displaystyle {\frac {a*(\;.\;)}{1*(2*3)}}}$
• 用語の各ノードには、その深さ(一部の著者は高さと呼ぶ)、つまりルートからの距離 (エッジの数) を割り当てることができます。この設定では、ノードの深さは常にその位置文字列の長さに等しくなります。図では、黒い用語の深さレベルが緑色で示されています。
• 用語のサイズは、一般的にそのノードの数、または括弧なしの記号を数えた用語の表記の長さを指します。図の黒い用語と青い用語のサイズは、それぞれ 15 と 5 です。
• 項u が 項tに一致するのは、 uの置換インスタンスが構造的にtの部分項に等しい場合、または形式的には、t内のある位置pとある置換 σに対してu σ = t | _pである場合です。この場合、 u、t、および σ は、それぞれパターン項、主題項、および一致する置換と呼ばれます。図では、青いパターン項⁠ ⁠ が位置 1 の黒い主題項に一致し、一致する置換{ x ↦ a、y ↦ a +1、 z ↦ a +2 }は、黒い置換のすぐ左にある青い変数によって示されています。直感的には、パターンは、その変数を除いて、主題に含まれている必要があります。変数がパターン内で複数回出現する場合、主題のそれぞれの位置に等しい部分項が必要です。${\displaystyle x*(y*z)}$
• 用語の統一
• 用語の書き換え

議論のドメインに基本的に異なる種類の要素が含まれている場合、すべての用語の集合をそれに応じて分割すると便利です。このために、各変数と各定数記号にソート（型と呼ばれることもあります）が割り当てられ、各関数記号にドメインソートと範囲ソートの宣言^{[注 3]}が割り当てられます。ソートされた項 f ( t ₁ ,..., t _n ) は、 i番目のサブ項のソートがfのi番目のドメインソートの宣言と一致する場合にのみ、ソートされたサブ項t ₁ ,..., t _nから構成されます。このような項は、適切にソートされているとも呼ばれます。その他の項（つまり、ソートされていないルールのみに従う項）は、適切にソートされていないと呼ばれます。

たとえば、ベクトル空間にはスカラー数の関連フィールドが付属しています。WとN をそれぞれベクトルと数のソートを表し、V _WとV _{N を}それぞれベクトル変数と数変数の集合、C _WとC _{N を}それぞれベクトル定数と数定数の集合とします。すると、たとえば、および0 ∈ C _Nであり、ベクトル加算、スカラー乗算、および内積はそれぞれ⁠ ⁠、および⁠ ⁠と宣言されます。変数シンボルおよびa、b ∈ V _Nを想定すると、項は整列されていますが、 は整列されていません ( + はソートNの項を 2 番目の引数として受け入れないため)。整列された項を作成するには、追加の宣言⁠ ⁠が必要です。複数の宣言を持つ関数シンボルは、オーバーロードされていると呼ばれます。 ${\displaystyle {\vec {0}}\in C_{W}}$${\displaystyle +:W\times W\to W,*:W\times N\to W}$${\displaystyle \langle .,.\rangle :W\times W\to N}$${\displaystyle {\vec {v}},{\vec {w}}\in V_{W}}$${\displaystyle \langle ({\vec {v}}+{\vec {0}})*a,{\vec {w}}*b\rangle }$${\displaystyle {\vec {v}}+a}$${\displaystyle a*{\vec {v}}}$${\displaystyle *:N\times W\to W}$

ここで説明するmany-sorted フレームワークの拡張を含む詳細については、many-sorted ロジックを参照してください。

表に示されている数学表記は、上で定義した第 1 階項のスキームには適合しません。これは、それらはすべて、表記のスコープ外には現れない可能性のある独自のローカル変数、または境界変数を導入するためです(例:は意味をなさない)。対照的に、自由と呼ばれるその他の変数は、通常の第 1 階項変数のように動作します (例: は意味をなさない)。 ${\displaystyle t\cdot \int _{a}^{b}\sin(k\cdot t)\;dt}$${\displaystyle k\cdot \int _{a}^{b}\sin(k\cdot t)\;dt}$

これらの演算子はすべて、引数の 1 つとして値項ではなく関数を取るものとして考えることができます。たとえば、lim演算子はシーケンス、つまり正の整数から実数などへのマッピングに適用されます。別の例として、表の 2 番目の例である Σ を実装するC関数には、関数ポインター引数があります (下のボックスを参照)。

ラムダ項は、 lim 、 Σ、 ∫ などの引数として渡される匿名関数を表すために使用できます。

たとえば、以下の C プログラムの関数square は、ラムダ項 λ i . i ²として匿名で記述できます。一般的な合計演算子 Σ は、下限値、上限値、および合計される関数を取る 3 項関数記号と考えることができます。後者の引数のため、 Σ 演算子は2 次関数記号と呼ばれます。別の例として、ラムダ項 λ n . x / n は、1、2、3、... をそれぞれx /1、x /2 、 x /3、... にマップする関数を表します。つまり、シーケンス( x /1、x /2、x /3、...) を表します。lim演算子は、このようなシーケンスを受け取り、その限界を返します (定義されている場合)。

表の右端の列は、各数学表記例をラムダ項でどのように表すことができるかを示しており、一般的な中置演算子を接頭辞形式に変換する方法も示しています。

int sum ( int lwb , int upb , int fct ( int )) { // 一般的な合計演算子を実装しますint res = 0 ; for ( int i = lwb ; i <= upb ; ++ i ) res += fct ( i ); return res ; }           
       
        
          
     


int square ( int i ) { return i * i ; } // 無名関数 (lambda i. i*i) を実装します。ただし、C では名前が必要です。                  

#include <stdio.h> int main ( void ) { int n ; scanf ( " %d" , & n ); printf ( "%d \n " , sum ( 1 , n , square )); // sum 演算子を適用して平方和を計算しますreturn 0 ; } 
  
     
    
               
     

変数シンボルの集合Vが与えられた場合、ラムダ項の集合は次のように再帰的に定義されます。

• すべての変数記号x ∈ Vはラムダ項である。
• x ∈ Vが変数記号であり、t がラムダ項である場合、 λ x . tもラムダ項である（抽象化）。
• t ₁とt _{2 が}ラムダ項である場合、( t ₁ t ₂ ) もラムダ項です（適用）。

上記の例では、 div、powerなどの定数も使用しましたが、これらは純粋なラムダ計算では認められていません。

直感的には、抽象 λ x . t は、xが与えられたときにtを返す単項関数を表し、アプリケーション ( t ₁ t ₂ ) は、入力t _2で関数t ₁を呼び出した結果を表します。たとえば、抽象 λ x . x は恒等関数を表し、 λ x . y は常にyを返す定数関数を表します。ラムダ項 λ x .( x x ) は関数xを受け取り、 x を自身に 適用した結果を返します。

• 方程式
• 表現（数学）

• フランツ・バーダー、トビアス・ニプコウ（1999年）。『用語の書き換えとその他すべて』ケンブリッジ大学出版局。pp. 1-2および34-35。ISBN 978-0-521-77920-3。