Coq é sintético ou analítico?

8

No curso HoTT da CMU, palestra 1, que pode ser encontrada aqui: https://scs.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=0945cc7f-48b7-4803-81af-e7193a3f461d

Às 33:52, Harper estava comparando paralelamente entre teorias sintéticas e analíticas, e quando chegou à teoria do PL, ele disse que Coq é analítico e disse que Coq apenas prova uma linguagem em sua gramática, mas não o analisador em si.

Tenho um forte desejo de discordar de alguma forma, mas não tenho uma ideia clara de por que gostaria de fazer isso. Eu acredito que o Coq é muito sintético, assim como qualquer outro assistente de prova baseado na teoria do tipo dependente, porque todas essas linguagens não fazem nada além de criar programas. Também podemos expressar álgebra axiomática em Coq usando classes de tipo, por exemplo, e concretizar sempre que adequado. Esse padrão é especialmente o caso da Agda.

Então, minha pergunta é: Harper estava certo? Se ele estiver certo, qual parte da minha opinião causa meu mal-entendido?

Jason Hu
fonte

Respostas:

12

A observação é sobre um uso específico do Coq, a formalização da teoria da linguagem de programação.

Vamos primeiro esclarecer a distinção entre sintético e analítico :

  • Numa abordagem sintética de um assunto, dizemos que existem coisas cujas propriedades e estrutura básicas são postuladas de uma maneira ou de outra. Em seguida, estudamos essas coisas confiando apenas nas propriedades e na estrutura postuladas.

  • Numa abordagem analítica de um assunto, descobrimos que existem certas coisas. Para aprender mais sobre eles, nós os separamos, estudamos como eles são feitos e os analisamos. Desta forma, descobrimos suas propriedades e estrutura.

Como alguém estudaria uma linguagem de programação dessas duas maneiras?

Sinteticamente, postularíamos as partes constituintes da linguagem (existem termos, existem tipos), sua estrutura básica (essas são as formas de construir termos) e propriedades básicas. Não perguntamos de que são feitos os termos e o tipo, ou se os termos são árvores ou seqüências de caracteres, ou se a coleção de tipos é construída de uma maneira específica.

Analiticamente, começaríamos com uma configuração matemática que nos permite fazer muitas coisas, como usar definições indutivas para construir objetos matemáticos. Construímos termos e tipos como conjuntos ou tipos específicos definidos indutivamente. Então estudaríamos sua estrutura, como podemos transformá-los, etc.

Deve ficar claro que Coq é do tipo analítico. Ao implementar uma linguagem de programação no Coq, você define tipos indutivos de termos e tipos. Em seguida, você os analisa usando indução, define semântica operacional como uma função recursiva na sintaxe dos termos, etc.

Por outro lado, Twelf é do tipo sintético. Postulamos que existe um tipo de termos e um tipo de tipos, mas não dizemos a Twelf que esses são tipos indutivos (não há como dizer isso em Twelf). Definimos semântica operacional, fornecendo regras básicas de transição. Não há menção de funções definidas recursivamente (não há como definir funções no Twelf), apenas confiamos nos postulados que escrevemos.

Você deve comparar a situação acima com a geometria planar. A abordagem de Hilbert à geometria é sintética (mas suas idéias estão enraizadas em Euclides), as de Descartes são analíticas. A geometria analítica é assim chamada porque uma linha não é um conceito primitivo: possui uma estrutura interna, ou seja, é um conjunto de pontos.

Andrej Bauer
fonte
Obrigado pela sua resposta. Você pode ver se minhas declarações a seguir estão alinhadas corretamente para verificar meu entendimento? 1. Ainda é possível fazer uma abordagem sintética no Coq, que é adotada, digamos, pela Unimath, proibindo o uso de definições indutivas. 2. O estudo das teorias de tipos em si é sintético, mas o estudo baseado nelas (assumindo o uso livre do recurso da linguagem) seria analítico. Se o HoTT for implementado como uma linguagem de programação, o uso do HIT e a indução o tornariam efetivamente um estudo analítico.
Jason Hu
O Unimath é sintético não porque não permite tipos indutivos, mas porque fala sobre tipos de homotopia sem analisar do que eles são feitos.
Andrej Bauer
@AndrejBauer - Estranhamente, essa distinção parece ser exatamente o oposto da filosofia, incluindo a filosofia da matemática . Lá, "analítico" significa declarações cujo significado depende apenas dos termos e de suas relações, sem ter que adicionar, "sintetizar", qualquer entrada externa (por exemplo, conhecimento factual sobre o estado do mundo). Portanto, nesse uso, Euclides seria analítico, enquanto Descartes envolveria a síntese de noções geométricas com noções algébricas (por exemplo, um ponto é um par (x, y) e uma linha é uma equação y = mx + b).
Diagon 21/07