누군가가 PCF에서 연속성 계수의 비 정의 가능성에 대한 참조를 지적 할 수 있습니까?

$\newcommand{\N}{\mathbb{N}}$

$\newcommand{\bool}{\mathsf{bool}}$

안드레이 바우어 (Andrej Bauer)는 몇 가지 문제에 대해 자세히 살펴 보는 아주 멋진 블로그 게시물 을 작성 했지만이 질문에 대한 문맥을 빌려주기 위해 그의 게시물 중 일부만 요약하겠습니다. Baire 공간 는 자연수 시퀀스의 집합이거나 자연수에서 자연수 N → N 까지의 함수 집합입니다 . 이 질문에 대해서는 계산 가능한 스트림으로 만주의를 제한 할 것입니다.B

$B$N→N

$\N \to \N$

이제, 함수 모든위한 경우 연속 X S ∈ B 의 값 F ( X S ) 의 요소의 한정된 수 의존 X 들 , 그리고 computably 연속있어 우리는 실제로 수 있다면 x 의 요소가 얼마나 필요한지 에 대한 상한을 계산하십시오 . 연산의 일부 모델에서,이 프로그램 작성 실제로 가능 m이 O D U L 유 이야 : ( B → B Of:B→bool

$f : B \to \bool$xs∈B

$xs \in B$f(xs)

$f(xs)$xs

$xs$xs

$xs$ Baire 공간과 Baire 공간의 요소에 대해 계산 가능한 기능을 수행하고 스트림의 요소 수에 대한 상한을 반환합니다.modulus:(B→bool)→B→N

$\mathsf{modulus} : (B \to \bool) \to B \to \N$

이를 구현하기위한 한 가지 트릭은 로컬 스토리지를 사용하여 최대 인덱스를 스트림에 기록하는 것입니다.

let modulus f xs =
  let r = ref 0 in
  let ys = fun i -> (r := max i !r; xs i) in
    f ys;
    !r

물론이 ys주장은 더 이상 순수하게 기능하는 프로그램이 아닙니다. 이 프로그램에 대한 관심은 지역 상점 만 사용한다는 점에서 비롯된 것이므로 확장 적으로 순수합니다. 나는 (다른 무엇보다도) 고차원 명령 프로그래밍을 연구하고 이것을 순수한 함수로 분류 할 수있는 유형 이론을 설계하고 있습니다.

메모 및 연결 풀링과 같은 실제적인 예제도 있지만 특히 아름다운 예입니다.

답변