関数記号 (Function Symbol)

関数記号は、指定された個数の引数を議論領域の要素へ写像する項の構成要素である。関数記号そのものは構文であり、具体的な写像は構造と解釈によって与えられる。

仕組みと確認

次数と解釈を定め、項を評価した結果が議論領域に戻ることを確認する。プログラムの関数では入力型、出力型、副作用、例外を数学的な全域写像と分けて記述する。

限界と注意点

部分関数や失敗を扱うには、エラーを領域に含めるか、別の意味論を採用する必要がある。関数という名前だけで決定性・停止性・副作用の不在を仮定しない。