言葉づかい、態度 2
ゲーデル化をどうするか? その2 - 檜山正幸のキマイラ飼育記 で、「コード」を問題にしたが、「述語」も大問題。
- 基本〈原子 | 原始〉述語記号〈述語名〉
- 定義された述語記号〈述語名〉
- 幾つかの変数を持つ論理式
- 論理式をボディに持つラムダ関数式〈ラムダ抽象〉
- 意味領域側の、任意のブール値関数
- 意味領域側の、論理式で表現可能なブール値関数
多項式と多項式関数は違うのと同じように、まったく任意のブール値関数(部分集合と同義)と、論理式で定義される関数は違う。濃度からして違う。
区別するなら:
- 述語記号=述語名
- n項の述語式=論理式をボディに持つラムダ関数式
- 述語関数は、述語式で定義される関数
計算可能性に関して、
- 計算的集合〈computational set〉=列挙付き集合〈enumerated set〉
幾つかの計算的集合と、計算的集合のあいだの幾つかの関数を、基本集合と基本関数として、計算可能圏〈computable category〉を作れる。計算可能圏の構成は、通常のデカルト圏構成以外に、再帰構成と計算的イプシロン記号〈computational epsilon〉を入れてよい。計算的イプシロン εx∈A.P は計算的集合〈データ領域〉A上の論理式Pに対して、P(a)が真であるaを返す手続き。aが存在しないなら⊥を返す。
再帰もイプシロンも、述語関数=計算可能ブール値関数という概念が必要なので、ブール値集合と、基本述語関数は前もって指定しておく必要がある。
述語関数=計算可能ブール値関数により、次の構成が可能となる。
- if文: if(p(x)) then f(x) else g(x)
- find文: find(x in D) p(x) ≡ for(x in D){if(p(x)) x}
付点集合を対象として、任意の写像を射とする圏を考えると、点を保つ写像の圏は、広い部分圏になる。この部分圏が通常の付点写像の圏で、部分写像の圏と同型。
具体的な計算可能圏は、付点写像の圏の部分圏であるが、充満部分圏ではない。
- fが計算可能 ⇒ fは付点写像(fはストリクト)
逆が成立しない。
非ストリクト関数は当然に計算可能ではない。計算可能の観点からの“超越関数”である。ここでの超越関数は、非代数的じゃなくて、非計算的の意味。