Loading article…
数理論理学において、項とは、式／公式の中で数学的対象を表す、従属／束縛記号の配列のことである。特に、項は公式の構成要素として現れる。これは自然言語における名詞句が対象を指し、文全体が事実を指すのと同様である。
1階項は、定数記号、変数記号、関数記号から再帰的に構成されます。適切な数の項に述語記号を適用して形成される式は原子式と呼ばれ、解釈が与えられた場合、二値論理では真または偽に評価されます。例えば、は定数 1、変数x、および二項関数記号から構成される項です。そして ; それは原子式の一部ですこれは、 xの実数値のそれぞれに対して真と評価されます。
変数記号の集合V 、定数記号の集合C 、およびn項関数記号（演算子記号とも呼ばれる）の集合F nが与えられたとき、各自然数n ≥ 1 に対して、(ソートされていない一階) 項の集合Tは、次の性質を持つ最小の集合として再帰的に定義されます。 [ 1 ]
直感的で擬似文法的な表記法を用いると、これは次のように書かれることがあります。
用語言語のシグネチャは、どの関数記号集合 F n が含まれるかを記述します。よく知られている例としては、単項関数記号sin、cos ∈ F 1と、二項関数記号+、 −、 ⋅、 / ∈ F 2があります。三項演算や高次関数も可能ですが、実際にはあまり一般的ではありません。多くの著者は定数記号を 0 項関数記号F 0とみなしており、そのため特別な構文クラスは必要ありません。
項は、議論領域からの数学的対象を表します。定数c はその領域からの特定の対象を表し、変数x はその領域内の対象を範囲とし、n項関数fはn個の対象の組を対象に対応付けます。たとえば、n ∈ Vが変数記号、1 ∈ Cが定数記号、add ∈ F 2 が二項関数記号である場合、第 1、第 2、第 3 項構成規則により、それぞれn ∈ T、1 ∈ T、そして (したがって) add ( n , 1) ∈ Tとなります。後者の項は、便宜上、中置記法とより一般的な演算子記号 +を使用して、通常はn +1と表記されます。
元々、論理学者は項を特定の構築規則に従う文字列として定義しました。[ 2 ]しかし、コンピュータサイエンスで木の概念が普及して以来、項を木として考える方が便利であることがわかりました。たとえば、「( n ⋅( n +1))/2」、「(( n ⋅( n +1)))/2」、「」などのいくつかの異なる文字列があります。、 は同じ項を表し、同じツリー、つまり上の図の左側のツリーに対応します。項のツリー構造を紙上のグラフィカルな表現から分離することで、括弧（構造ではなく表現のみ）や目に見えない乗算演算子（表現ではなく構造のみに存在する）も簡単に説明できます。
2 つの項は、同じツリーに対応する場合、構造的に、文字通り、または構文的に等しいと言われます。たとえば、上の図の左と右のツリーは、構造的に等しくない項ですが、有理数演算では常に同じ値に評価されるため、 「意味的に等しい」と見なされる場合があります。構造的等価性は記号の意味を知らなくても確認できますが、意味的等価性は確認できません。たとえば、関数 / が有理数ではなく 切り捨て整数除算として解釈される場合、 n = 2のとき、左と右の項はそれぞれ 3 と 2 に評価されます。構造的に等しい項は、変数名が一致する必要があります。
対照的に、項tは、項uのすべての変数を一貫して名前変更することによって得られた場合、つまり、何らかの名前変更置換 σ に対して u = tσ である場合、項uの名前変更、または変形と呼ばれます。この場合、名前変更置換 σ には逆 σ −1があり、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 0、i項関数の記号の数をf iと略記すると、高さhまでの異なる基底項の数 θ h は、次の漸化式で計算できます。
各自然数n ≥ 1 に対してn項関係記号の集合R nが与えられたとき、 n項にn項関係記号を適用することで (ソートされていない一階) 原子式が得られます。関数記号の場合と同様に、関係記号集合R nは通常、 nが小さい場合にのみ空ではありません。数理論理学では、論理結合子と量化子を使用して原子式からより複雑な式が構築されます。たとえば、ℝ を実数の集合とすると、∀ x : x ∈ ℝ ⇒ ( x +1)⋅( x +1) ≥ 0は複素数代数で真となる数学式です。原子式は、完全に基礎項から構築されている場合、基礎と呼ばれます。与えられた関数記号と述語記号の集合から構成可能なすべての基礎原子式は、これらの記号集合のヘルブランド基底を構成します。
議論領域に基本的に異なる種類の要素が含まれる場合、すべての項の集合をそれに応じて分割することが有用です。この目的のために、各変数と各定数シンボルにソート（型とも呼ばれる）が割り当てられ、各関数シンボルに領域ソートと範囲ソートの宣言[注3 ]が割り当てられます。ソートされた項f ( t 1 ,..., t n ) は、 i番目の部分項のソートがfの宣言されたi番目の領域ソートと一致する場合に限り、ソートされた部分項t 1 ,... , t nから構成できます。このような項は、適切にソートされているとも呼ばれます。その他の項（つまり、ソートされていない規則のみに従う項）は、不適切にソートされていると呼ばれます。
例えば、ベクトル空間にはスカラー数の関連体があります。WとNをそれぞれベクトルと数の型とし、VWとVNをそれぞれベクトル変数と数変数の集合、CWとCNをそれぞれベクトル定数と数定数の集合とします。すると、例えば0 ∈ C Nであり、ベクトル加算、スカラー乗算、内積は次のように宣言されます。、そしてそれぞれ。変数記号を仮定するとまた、a、b ∈ V N の場合、項よく整理されているが、（+ は 2 番目の引数としてN型の項を受け入れないため）そうではありません。きちんと整理された用語、追加の宣言が必要です。複数の宣言を持つ関数シンボルはオーバーロードされていると呼ばれます。
多ソートロジックに関する詳細情報、およびここで説明する多ソートフレームワークの拡張機能については、そちらを参照してください。
表に示す数学的表記法は、上記で定義した一次項の枠組みには当てはまりません。なぜなら、それらはすべて、表記法の範囲外では現れない可能性のある独自の局所的または境界変数を導入するからです。意味がありません。対照的に、自由変数と呼ばれる他の変数は、通常の一次項変数のように振る舞います。例:なるほど、納得です。
これらの演算子はすべて、引数として値ではなく関数を受け取るものと見なすことができます。たとえば、lim演算子は数列、つまり正の整数から実数への写像に適用されます。別の例として、表の2番目の例であるΣを実装するC関数は、関数ポインタ引数を持ちます（下のボックスを参照）。
ラムダ項は、 lim、Σ、∫などの引数として提供される匿名関数を表すために使用できます。
例えば、以下の C プログラムの関数square は、ラムダ項 λ i . i 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 ; }// 匿名関数 (lambda i. i*i) を実装していますが、C 言語では名前が必要です。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 )); // 平方数を合計するために合計演算子を適用しますreturn 0 ; }変数記号の集合Vが与えられたとき、ラムダ項の集合は次のように再帰的に定義される。
上記の例では、 div、powerなどの定数も使用しましたが、これらは純粋なラムダ計算では認められていません。
直感的に、抽象化 λ x . t は、 xが与えられたときにtを返す単項関数を表し、適用 ( t 1 t 2 ) は、入力t 2で関数t 1を呼び出した結果を表します。たとえば、抽象化 λ x . x は恒等関数を表し、λ x . y は常にyを返す定数関数を表します。ラムダ項 λ x .( x x ) は関数xを受け取り、 xをそれ自身に適用した結果を返します。