Implementando idiomas "internos"

11

Uma das conseqüências mais práticas da correspondência "Curry-Howard-Lambek" é que a sintaxe de muitas lambda-calucli / lógicas pode ser usada para executar construções em uma categoria suficientemente estruturada.

Por exemplo, a Geometria Diferencial Sintética possui modelos nos topos que contêm e incorporam a categoria de coletores suaves, para que você possa usar a lógica de ordem superior para construir funções suaves e resolver equações diferenciais.

Como outro exemplo, neste artigo , eles notam que a "indexação por etapas" está realmente apenas trabalhando com pré-misturas sobre os naturais (outro topos), para que você possa usar a sintaxe da lógica de ordem superior para definir relações lógicas indexadas por etapas sem o tedioso manipulação de etapas.

Finalmente, Andrej Bauer mostra nesta pergunta do MO que você pode fazer muito com a "linguagem interna" dos topos dos gráficos.

Minha pergunta é: alguém já realizou essa visão literalmente em um provador de teoremas ? Por exemplo, se eu mostrar que uma categoria com a qual me preocupo é Fechada Cartesiana, poderia passar para o "modo interno", onde escrevo a sintaxe lambda-calculus (com alguns axiomas específicos do modelo) e depois voltar para o "modo externo" e manipulá-los como objetos no meu modelo?

No extremo, eu iria querer a teoria do topos e a lógica de ordem superior, para poder escrever minhas relações lógicas indexadas por etapas sem etapas ou ensinar mecânica clássica com um provador de teoremas usando SDG. Parece-me uma idéia muito poderosa, já que alguém poderia implementar a teoria de tipos dependentes extensional uma vez e fornecer ferramentas agradáveis ​​e usá-las com aplicativos totalmente diferentes, conforme descrito acima.

Max Novo
fonte
Apenas por uma questão de clareza: você está perguntando se alguém já reescreveu uma teoria matemática na linguagem interna da categoria subjacente (por usar o provador de teoremas para provar coisas dessas teorias matemáticas)? Ou você está interessado em saber se alguém já fez a teoria dos modelos na teoria dos tipos (de algum tipo de categoria)?
Giorgio Mossa
Não estou perguntando sobre o trabalho que as pessoas fizeram em uma determinada linguagem interna em um provador de teoremas (embora as referências sejam bem-vindas). Estou perguntando se alguém fez o trabalho de implementar "Linguagens Internas" como essencialmente DSLs em um provador de teoremas, para que eu possa usar a linguagem interna para qualquer modelo específico em que me interesse e obter todos os benefícios de uma boa sintaxe. Para os CCCs, isso parece fácil, pois a sintaxe pode ser facilmente expressa em Coq / Agda etc., mas o Topoi parece mais difícil.
Max New

Respostas:

7

Em Extendendo a Teoria dos Tipos com Forçamento, de Guilhem Jaber, Nicolas Tabareau e Matthieu Sozeau, 2012, a forçagem intuicionista é apresentada como uma internalização da construção pré-folga, implementada como uma tradução de preservação de tipo no estilo da tradução da parametridade de Bernardy e Lasson .

Isso significa que você pode definir termos em sua teoria de tipos usual e "traduzi-los" em uma "camada forçada", onde eles são interpretados como traduções em um tipo de tradução diferente. Por exemplo, a tradução induzida pela indexação em números naturais decrescentes permite que você use seus termos habituais em uma teoria pós-tradução em que uma latermodalidade é definível. Isso parece muito próximo da sua ideia de trabalhar internamente nos topos das árvores.

Parece que eles têm um novo e mais simples plugin Coq implementando essas idéias no CoqHott / coq-forcing , e em particular o SI.v constrói essa tradução forçada para indexação por etapas. Infelizmente, embora ele faça o trabalho de construir o modelo, não há exemplo para utilizá-lo para definições indexadas por etapas na prática (a única coisa traduzida em vez de definida na camada forçadora é Forcing Translate eq, o que não é muito informativo). Você pode experimentar para ver como (in) isso é conveniente.

gasche
fonte
5

Se você estiver trabalhando apenas no idioma interno, poderá usar um assistente de prova. Existe um pequeno detalhe técnico de ter ou não conjuntos de potências, já que os assistentes de prova são tipicamente teorias de tipos, mas o Coq Propé consistente com uma interpretação do Coq em um topos.

No entanto, você está sugerindo o uso da máquina como uma ferramenta de tradução que o levaria do idioma interno para a interpretação em um modelo. Essa é uma boa idéia, exceto que eu acho que não seria tão útil quanto se poderia esperar. É verdade que a tradução do idioma interno para o modelo é mecânica, mas infelizmente produz traduções complicadas que precisam de muita massagem antes de serem úteis. (Se você já tentou usar a interpretação de Lawos Tope-Tierney da lógica topos em um topos de feixe, você saberá.)

Há mais um problema, a tradução reversa . Geralmente começamos com um conceito ou objeto conhecido no modelo e gostaríamos de uma boa descrição ou axomatização dele na linguagem interna. Isso normalmente é trabalho duro e matemática real. Não vejo como os assistentes de provas atuais poderiam ajudar.

No lado técnico, é preciso se preocupar em formalizar:

  • a sintaxe e as regras da linguagem interna
  • o modelo
  • a interpretação

λ

Em resumo, usar um assistente de prova para ajudar a verificar se você não está fazendo nada errado na linguagem interna é uma boa ideia (na verdade, é uma ideia muito boa, como atestado pela teoria do tipo de homotopia, em que usamos Coq e Agda para desenvolver novos teoremas que apenas foram posteriormente não-formatados para o inglês), mas é improvável que usá-lo para obter declarações sobre modelos funcione sem muito trabalho extra. O que não quer dizer que você não deva tentar!

Andrej Bauer
fonte
Você tem uma referência para Type Theory + Prop ~~ topos? Essa foi a minha intuição, mas eu não vi mais ninguém dizer isso até agora.
Max New
Além disso, para lógicas específicas de modelo, axiomas específicos serão específicos para os modelos, mas a estrutura da lógica geral ainda é apenas lógica de ordem superior, certo? Imagino que você caracterize externamente os recursos do seu modelo (como o functor da próxima vez no documento de indexação por etapas) e depois os reflita como axiomas em sua linguagem interna. Criar axiomatizações legais e completas ainda seria difícil, mas minha esperança é que a máquina possa automatizar parte do encanamento.
Max New
Para indexação por etapas, em particular, faria sentido estender a lógica do topos com um operador modal. Este será em geral uma característica de qualquer situação em que você se preocupa com um subtopos, ou você tem um (co) mônada que você quer estudar, etc.
Andrej Bauer
Para a teoria dos tipos + Prop, você apenas observa todas as regras e vê que, se interpretar Prop como o classificador de subobjeto, tudo é válido em um topos.
Andrej Bauer