Referência para a indefinibilidade do módulo de continuidade funcional no PCF?

10

Alguém pode me apontar a referência para a não definibilidade do módulo de continuidade funcional no PCF? \ newcommand {\ bool} {\ mathsf {bool}}

Andrej Bauer escreveu um post muito bom no blog explorando alguns dos problemas com mais detalhes, mas vou resumir apenas um pouco do seu post para dar algum contexto a essa pergunta. O espaço de Baire B é o conjunto de sequências de números naturais, ou equivalentemente o conjunto de funções do naturais para naturais NN . Para esta questão, restringiremos nossa atenção apenas aos fluxos que são computáveis.

Agora, uma função f:Bbool é contínua se, para cada xsB , o valor de f(xs) depende apenas de um número finito dos elementos de xs , e é computacionalmente contínua se, na verdade, pudermos calcular um valor superior limitado a quantos elementos de xs são necessários. Em alguns modelos de computação, é realmente possível escrever um programa modulus:(Bbool)BN que assume uma função computável no espaço Baire e um elemento do espaço Baire, e devolve o limite superior do número de elementos do fluxo.

Um truque para implementar isso é usar o armazenamento local para registrar o índice máximo no fluxo visto:

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

Obviamente, o ysargumento não é mais um programa puramente funcional. Meu interesse neste programa vem do fato de que ele apenas utiliza lojas locais e, portanto, é extensionalmente puro. Trabalho (entre outras coisas) em programação imperativa de ordem superior e estou projetando teorias de tipos que poderiam classificá-la como uma função pura.

Também existem exemplos mais práticos, envolvendo coisas como memorização e pool de conexões, mas acho esse um exemplo particularmente bonito.

Neel Krishnaswami
fonte

Respostas:

4

A prova está escondida em algum lugar de Troelstra e van Dalen, Construtivismo em matemática, volume 2, suponho. Provavelmente, isso pode ser encontrado nas investigações de Troelstra , se você puder pôr as mãos nela.

É assim. Suponha que possamos definir o módulo de continuidade em -calculus digitado com operadores de ponto de fixação. Em seguida, poderíamos interpretá-lo em um modelo de realização teórico de domínio, por exemplo, em onde é o modelo gráfico de Scott. Nesse modelo, o princípio de escolha é válido. Mas sabe-se que juntamente com a extensionalidade de funções (que é válida em todo modelo de realização), é incompatível com a existência de módulo de continuidade. Se eu tiver um momento, preencherei os detalhes mais tarde.λPER(Pω)PωAC2,0AC2,0

Veja também M. Escardo, T. Streicher: Na realizabilidade de domínio, nem todos os funcionais são contínuos , publicado em Mathematics Logic Quarterly, volume 48, edição Suplemento 1, páginas 41-44, 2002 .

Andrej Bauer
fonte
Eu procurei por isso. Está em "Construtivismo em matemática, volume 2", de Troelstra e van Dalen, seção 6.10, página 500. Acho que vou colocar isso no meu blog porque é muito difícil de encontrar.
Andrej Bauer
Obrigado! Qual é o axioma ? AC2,0
Neel Krishnaswami
AC(X,Y) é e são . (xXyY.R(x,y))fYXxX.R(x,f(x))AC2,0AC(NNN,N)
Andrej Bauer
Ok, aqui está a metade da prova: math.andrej.com/2011/07/27/…
Andrej Bauer