O que se entende por teoria das categorias ainda não sabe como lidar com funções de ordem superior?

Ao ler a resposta de Uday Reddy a Qual é a relação entre os functores na SML e na teoria das categorias? Uday estados

A teoria das categorias ainda não sabe como lidar com funções de ordem superior. Algum dia, será.

Como eu pensava que a teoria das categorias pudesse servir de base para a matemática, deveria ser possível derivar todas as funções matemáticas e de ordem superior.

Então, o que se entende por teoria das categorias ainda não sabe como lidar com funções de ordem superior? É válido considerar a teoria das categorias como fundamento da matemática?

O problema com funções de ordem superior é simples o suficiente para declarar.

• Um construtor de tipo como não é um functor. Deveria ter sido. $T(X) = [X \to X]$

• Uma função polimórfica como não é uma transformação natural. Deveria ter sido.${\it twice}_X : T(X) \to T(X) = \lambda f.\, f \circ f$

Se você ler o artigo de teoria das categorias original de Eilenberg e MacLane , (PDF), as intuições apresentadas apresentam esses casos. Mas a teoria deles não. O trabalho deles foi ótimo para 1945! Mas hoje precisamos de mais.

A reação dos teóricos da categoria a essas questões é um pouco desconcertante. Eles agem como se operações de ordem superior formem uma idéia de Ciência da Computação; eles não têm importância para a matemática. Se é assim, um fundamento da matemática não seria bom o suficiente para um fundamento da ciência da computação.

Mas não acredito seriamente nisso. Acredito que funções de ordem superior também seriam importantes para a matemática. Mas eles não foram seriamente explorados. Espero que, algum dia, eles sejam explorados e que as limitações da teoria das categorias sejam realizadas.

[Esta segunda resposta apresenta um esboço de como pode ser uma "Teoria da categoria 2.0", que lida corretamente com funções de ordem superior.]

Já sabemos há muito tempo como lidar com funções de ordem superior no raciocínio sobre elas.

• Quando uma estrutura algébrica possui operações de ordem superior, os homomorfismos não funcionam. Em vez disso, devemos usar relações lógicas . Em outras palavras, devemos passar de " funções preservando estrutura" para " relações preservando estrutura".

• Para falar sobre transformações "uniformes" ou "dadas simultaneamente" em tipos de ordem superior, a naturalidade não funciona. Devemos usar a parametridade relacional . Em outras palavras, devemos passar de "famílias preservando todos os morfismos " para "famílias preservando todas as relações lógicas ".

• $\to$

Uma rápida introdução a essas questões está na seção de Peter O'Hearn sobre "Parametricidade relacional" em domínios e semântica denotacional: história, realizações e problemas em aberto (CiteSeerX) .

• A primeira tentativa de construir uma "Teoria da categoria 2.0" está na Parametridade e variáveis ​​locais de O'Hearn e Tennent (CiteSeerX) .

• Tese de doutorado de Brian Dunphy: Parametridade como noção de uniformidade em gráficos reflexivos (CiteSeerX) baseia-se em sua estrutura e axiomatiza a estrutura relacional necessária para obter resultados de parametridade. Eu recomendaria a tese de Dunphy para obter uma boa visão geral de todos os problemas.

• Por uma questão de completude, devo mencionar também a tese de doutorado de Claudio Hermida: fibrações, predicados lógicos e indeterminados (PDF) , que foi o primeiro a estudar relações lógicas em um cenário teórico de categoria, mas seu tratamento talvez seja técnico demais para a maioria das pessoas.

Também devo acrescentar que o raciocínio sobre o estado é onde as funções de ordem superior aparecem com destaque. Os teóricos dos autômatos foram os primeiros a reconhecer que os homomorfismos não funcionam corretamente, em um artigo histórico chamado Produtos de Autômatos e o Problema da Cobertura . Eles usaram termos como "homomorfismos fracos" e "relações de cobertura" para se referir a relações lógicas. No devido tempo, termos como "simulação" e "bisimulação" foram usados ​​para se referir a eles. Artigo de pesquisa de Davide Sangiorgi: Sobre as origens da bisimulação e coindução abrange toda essa história inicial e muito mais.

A necessidade de raciocínio relacional surge repetidamente no raciocínio sobre o estado, em particular na programação imperativa . Muito poucas pessoas percebem que o humilde ponto e vírgula é uma operação de ordem superior. Portanto, você não pode decolar pensando em programas imperativos sem saber como lidar com funções de ordem superior. Continuamos ignorando as questões de estado e programação imperativa na crença equivocada de que a matemática tem todas as respostas. Portanto, se os matemáticos não entendem o estado, não deve ser bom! Nada poderia estar mais longe da verdade. O estado está no coração da Ciência da Computação. Avançaremos a ciência em geral, mostrando às pessoas como lidar com o estado!