Ссылка для неопределимости модуля непрерывности функционала в ПКФ?

Может ли кто-нибудь указать мне на ссылку на неопределяемость модуля функционала непрерывности в PCF? $\newcommand{\N}{\mathbb{N}}$ $\newcommand{\bool}{\mathsf{bool}}$

Андрей Бауэр написал очень хороший пост в блоге, в котором более подробно рассматриваются некоторые вопросы, но я кратко изложу его пост, чтобы дать некоторый контекст этому вопросу. Бэровский этом множество последовательностей натурального числа, или , что эквивалентно множество функций от натуралий к Naturals N → N . В этом вопросе мы ограничимся только потоками, которые можно вычислить.$B$$\N \to \N$

Теперь функция непрерывна, если для каждого x s ∈ B значение f ( x s ) зависит только от конечного числа элементов x s , и оно вычислимо непрерывно, если мы действительно можем вычислить верхнюю границу на сколько элементов х годов необходимы. В некоторых моделях вычислений, это на самом деле можно написать программу т о д у л у ев : ( B → B $f : B \to \bool$$xs \in B$$f(xs)$$xs$$xs$ который принимает вычислимую функцию на пространстве Бэра и элемент пространства Бэра и возвращает верхнюю границу для числа элементов потока.$\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аргумент больше не является чисто функциональной программой. Мой интерес к этой программе исходит из того , что он делает только использование местного магазина, и поэтому является экстенсионально чистым. Я работаю (помимо прочего) с императивным программированием высшего порядка и разрабатываю теории типов, которые могли бы классифицировать это как чистую функцию.

Есть и более практичные примеры, такие как запоминание и пул соединений, но я считаю это особенно красивым примером.

Доказательство спрятано где-то в Troelstra и van Dalen, Конструктивизм в математике, том 2, я полагаю. Скорее всего, это можно найти в расследованиях Troelstra , если вы можете возложить на это руки.

$\lambda$$\mathsf{PER}(\mathcal{P}\omega)$$\mathcal{P}\omega$$AC_{2,0}$$AC_{2,0}$

См. Также М. Эскардо, Т. Штрайхер: В реализуемости домена не все функционалы непрерывны , опубликовано в « Математической логике ежеквартально», том 48, выпуск 1, стр. 41–44, 2002 .