바 재귀
Bar recursion바 재귀는 C가 개발한 일반화된 형태의 재귀다.스펙터는 1962년 논문을 썼다.[1]원시적 재귀가 통상적인 유도와 관련되거나, 트랜스피나이트 재귀가 트랜스피나이트 유도와 관련되는 것과 같은 방식으로 바 유도와 관련이 있다.
기술 정의
V, R, O를 유형으로 하고, 나는 V에서 추출한 일련의 파라미터를 나타내는 임의의 자연수가 된다.다음i+n 경우 V → R - O의 함수 f의n 함수 f는 다음과nn 같은 경우 B : ((Vi+n → R) x (Vn → R) → O의 함수 L : R → O 및 B로부터의 바 재귀에 의해 정의된다.
- fn(λα:Vi+n)r = r의 어떤 연장에서의 L이n+k L과n 같을 정도로 충분히 긴 r의 Ln(r)이다.L이 연속 시퀀스라고 가정하면 연속 함수는 미세하게 많은 데이터만 사용할 수 있기 때문에 이러한 r이 있어야 한다.
- fni+n(p) = V → R의 모든 p에 대한 Bn(p, (px:V)fn+1(cat(p, x)))
여기서 "cat"은 연결함수로 p, x를 p로 시작하는 시퀀스에 보내고 x를 마지막 용어로 한다.
(이 정의는 에스카르도와 올리바에 의한 정의에 근거한다.)[2]
Vi → R 유형의 모든 충분히 긴 함수( (α)r에 대해n L(r) = Bn(λα)r, ( (x:V)Ln+1(r)가 있는 일부 n이 있는 경우 바 유도 규칙은 f가 잘 정의되어 있음을 보장한다.
아이디어는 V에 걸쳐 시퀀스 트리의 충분히 긴 노드에 도달할 때까지 효과를 결정하기 위해 반복 용어 B를 사용하여 시퀀스를 임의로 확장한 다음, 기준 용어 L이 f의 최종 값을 결정한다는 것이다.잘 정의된 조건은 모든 무한 경로가 결국 충분히 긴 노드, 즉 막대 유도를 실행하는 데 필요한 요구 조건을 통과해야 한다는 요건에 해당한다.
바 유도와 바 재귀의 원리는 의존적 선택의 공리의 직관적 등가물이다.[3]
참조
- ^ C. Spector (1962). "Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics". In F. D. E. Dekker (ed.). Recursive Function Theory: Proc. Symposia in Pure Mathematics. Vol. 5. American Mathematical Society. pp. 1–27.
- ^ Martín Escardó; Paulo Oliva. "Selection functions, Bar recursion, and Backwards Induction" (PDF). Math. Struct. in Comp.Science.
- ^ Jeremy Avigad; Solomon Feferman (1999). "VI: Gödel's functional ("Dialectica") interpretation". In S. R. Buss (ed.). Handbook of Proof Theory (PDF).
