Uma categoria fechada bicartesiana de ordens parciais completas estritas (Hask)

8

Parece ser sabido que as linguagens de programação não podem ter somas, produtos e não-terminação juntos.

Q1 . Isso é verdade? Abaixo (ou no link acima que eu dei) está um argumento parcial.

No entanto, a programação genérica de Hinze com adições ignora a questão, mesmo depois de discutir um pouco precisamente qual é a categoria envolvida. Em particular, ele fala (aparentemente sem reservas) sobre Haskell ser modelado pela categoria de pedidos parciais contínuos e estritos e de somas e produtos. Mas sabemos que Haskell não tem somas (certo?). (A parte dos usos de papel S e T em vez, mas que não permite a não terminação).SCpoSet

Q2 Então, o que estou perdendo? Eu vejo quatro opções:

  • As pessoas geralmente ignoram a não rescisão de propósito quando discutem Haskell. Talvez este artigo também o faça. Mas por que alguém mencionaria CPOs então?
  • A barreira que discuto pode ser evitada de maneiras inteligentes. Em particular, os modelos de papel não rigorosas funções Haskell por funções estritas f : Um B , por outras razões.f:ABf:AB
  • O artigo menciona a limitação e eu perdi isso. Eu gastei algum esforço procurando por essa menção e não encontrei nenhuma.
  • Este é um erro real e, como todo mundo continua reivindicando Haskell, de fato, carece de somas categóricas (como outras pessoas concordam), mesmo que o jornal afirme Eitherser uma coisa dessas. Tudo funciona bem, em vez disso, em idiomas totais, com tipos indutivos e coindutivos.

fundo

AA×1A×00A

Isso significa, por exemplo, que a categoria de conjuntos pontiagudos , com seu objeto zero, não pode ser fechada bicartesiana.

ωCPOCPO

Blaisorblade
fonte

Respostas:

11

Sim, é impossível ter um CCC não regenerado com recursão geral e coprodutos categóricos. A referência padrão para isso é:

H. Huwig e A. Poigne. Uma observação sobre inconsistências causadas por pontos de correção em uma categoria fechada cartesiana. Teórica Computer Science, 73: 101–112, 1990.

No entanto, eu e (a maioria das outras pessoas que conheci) aprendemos sobre isso no capítulo do manual de Achim Jung e Samson Abramsky, Domain Theory , que eles gentilmente disponibilizaram gratuitamente.

A maioria das categorias de domínios com as quais as pessoas trabalham são subcategorias do DCPO, a categoria de pré-domínios e funções contínuas neles. Como os domínios pré-domínios não necessariamente têm um ponto mínimo fixo, essa categoria é um bi-CCC, mas existem pontos fixos apenas para funções em domínios.

Na página 46 destas anotações, há uma grande tabela informando em que subcategoria de DCPO diferentes construções existem.

Neel Krishnaswami
fonte