Loading article…
バー再帰は、 C.スペクターが1962年の論文で開発した再帰の一般化された形式です。[1]バー再帰とバー帰納法の関係は、原始再帰が通常の帰納法と関連しているのと同じように、また超限再帰が超限帰納法と関連しているのと同じです。
技術的な定義
V、R、およびOを型とし、iをVから取得したパラメータのシーケンスを表す任意の自然数とします。このとき、 V i + n → RからOへの関数f nの関数シーケンスf は、関数L n : R → OおよびBからのバー再帰によって定義され、 B n : (( V i + n → R ) x ( V n → R )) → Oの場合:
- f n ((λα: V i + n ) r ) = L n ( r ) であり、r は十分長く、rの任意の拡張上のL n + kはL n に等しくなります。Lが連続シーケンスであると仮定すると、連続関数は有限量のデータしか使用できないため、このようなrが存在する必要があります。
- V i + n → Rの任意のpに対して、 f n ( p ) = B n ( p , (λ x : V ) f n +1 (cat( p , x ))) となる。
ここで、「cat」は連結関数であり、p、x を、pで始まり最後の項が xであるシーケンスに送信します。
（この定義はエスカルドとオリバの定義に基づいています。[2]）
V i → R型の十分に長い関数 (λα) rごとに、 L n ( r ) = B n ((λα) r , (λ x : V ) L n +1 ( r ) を満たすnが存在すると仮定すると、バー帰納法の規則により、 f が明確に定義されることが保証されます。
その考え方は、再帰項B を使用して効果を決定し、V上のシーケンスのツリーの十分に長いノードに到達するまでシーケンスを任意に拡張し、次に基本項Lによってfの最終値を決定するというものです。明確に定義される条件は、すべての無限パスが最終的に十分に長いノードを通過する必要があるという要件に対応します。これは、バー帰納法を呼び出すために必要な要件と同じです。
バー帰納法とバー再帰の原理は、従属選択公理の直観主義的等価物である。[3]
参考文献
- ^ C. Spector (1962)。「解析の証明可能な再帰的関数: 現在の直観主義数学の原理の拡張による解析の一貫性証明」。FDE Dekker (編)。再帰関数理論: 純粋数学シンポジウム講演集。第 5 巻。アメリカ数学会。pp. 1–27。
- ^ マルティン・エスカルド;パウロ・オリバ。 「選択関数、バー再帰、および後方帰納法」(PDF)。数学。構造体。コンプサイエンス。
- ^ Jeremy Avigad ; Solomon Feferman (1999). 「VI: Gödel の機能的 (「弁証法」) 解釈」。SR Buss (編) 『証明理論ハンドブック』(PDF)。