数式

出典: フリー百科事典『ウィキペディア（Wikipedia）』

数式（すうしき、mathematical expression, mathematical formula）とは、数・演算記号・不定元などの数学的な文字・記号（および約物）が一定の規則にのっとって結合された、文字列のことである。

一般に数式には、その値 (value) とよばれるものが定められており、数式はその値を表現するものであると考えられている。数式の値の評価 (evaluation) は、その数式に用いられる記号の定義あるいは値によって決まる。すなわち、数式はそれが現れる文脈に完全に依存した形で決まるのである。

数式には独立変数（free variable; 自由変数）あるいは不定元と呼ばれる、その数式自体の中では値を持たないような記号を含むものも存在する。独立変数の評価は数式を含む文脈から外因的に与えられるのである。対して従属変数（bound variables; 束縛変数）と呼ばれる記号はその評価が特定の独立変数に結び付けられており、その対応する独立変数の評価が行われ値が決定されるごとに、従属変数自身の評価が同時に（従属的に）行われる

二つの数式が同値であるとは、その二つの数式が同じ値に結び付けられていることを言う。

数式やその評価について、その定式化は、1930年代のアロンゾ・チャーチやステファン・クリーンのラムダ計算によってなされている。ラムダ計算は現代数学や計算機におけるプログラミング言語の発展に多大な影響をもたらした。

ラムダ計算の興味深い結果の一つに、ラムダ計算において二つの数式が同値かどうか決定不能な場合が存在するというのが挙げられる。これはまた、ラムダ計算に等価な能力を持つ任意の系の、任意の数式にもあてはまる。