Definições construtivas padrão de números inteiros, racionais e reais?

Números naturais são definidos indutivamente como (usando a sintaxe Coq como exemplo)

Inductive nat: Set :=
| O: nat
| S: nat -> nat.

Existe uma maneira padrão de definir números inteiros (e talvez outros conjuntos como racionais e reais) construtivamente?

Existem várias maneiras de definir uma estrutura matemática, dependendo de quais propriedades você considera a definição. Entre caracterizações equivalentes, qual você considera a definição e qual você considera uma caracterização alternativa não é importante.

Na matemática construtiva, é preferível escolher uma definição que facilite o raciocínio construtivo. Para números naturais, a forma básica de raciocínio é a indução, o que torna a definição tradicional de zero ou sucessor muito adequada. Outros conjuntos de números não têm essa preferência.

Ao raciocinar sobre quocientes, em configurações não construtivas, é comum dizer "escolha um membro da classe de equivalência". Em um cenário construtivo, é necessário descrever como escolher um membro. Isso facilita as definições que constroem um objeto para cada membro do tipo, em vez de construir classes de equivalência.

$\mathbb{Z}$

Inductive Z1 :=
  | Nonnegative : nat -> Z1   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Negative : nat -> Z1.     (* ⟦Negative x⟧ = -⟦x⟧-1 *)

No entanto, essa definição é estranhamente assimétrica, o que pode tornar preferível admitir duas representações diferentes para zero:

Inductive Z2 :=
  | Nonnegative : nat -> Z2   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Nonpositive : nat -> Z2.  (* ⟦Nonpostitive x⟧ = -⟦x⟧ *)

Ou podemos construir os números inteiros relativos sem usar os naturais como um bloco de construção:

Inductive Pos3 :=
  | I : Pos3                  (* ⟦I⟧ = 1 *)
  | S3 : Pos3 -> Pos3         (* ⟦S3 x⟧ = ⟦x⟧+1 *)
Inductive Z3 :=
  | N3 : Pos3 -> Z3           (* ⟦N3 x⟧ = -⟦x⟧ *)
  | O3 : Z3                   (* ⟦O3⟧ = 0 *)
  | P3 : Pos3 -> Z3           (* ⟦P3 x⟧ = ⟦x⟧ *)

Os usos da biblioteca padrão Coq ainda outra definição: constrói inteiros positivos da sua notação de base 2 é, como o dígito 1 seguido por uma sequência de dígitos 0 ou 1. É então constrói Zcomo Z3a partir Pos3de cima. Essa definição também possui uma representação exclusiva para cada número inteiro. A escolha de usar notação binária não é para facilitar o raciocínio, mas para produzir código mais eficiente quando programas são extraídos de provas.

A facilidade de raciocínio é uma motivação para escolher uma definição, mas nunca é um fator intransponível. Se alguma construção facilitar uma prova específica, é possível usar essa definição nessa prova específica e provar que a construção é equivalente à outra construção que foi escolhida originalmente como definição.

$\mathbb{N}$Q$\mathbb{N} \times \mathbb{N}^*$=?=Q

Os números reais são uma chaleira diferente, porque não são construtíveis. É impossível definir os números reais como um tipo indutivo (todos os tipos indutivos são denumeráveis). Em vez disso, qualquer definição dos números reais deve ser axiomática, ou seja, não construtiva. É possível construir subconjuntos denumeráveis ​​dos números reais; a maneira de fazer isso depende do subconjunto que você deseja construir.

A resposta de Gilles é boa, exceto pelo parágrafo sobre os números reais, que é completamente falso, exceto pelo fato de que os números reais são de fato uma chaleira diferente de peixe. Como esse tipo de desinformação parece ser bastante difundido, eu gostaria de registrar aqui uma refutação detalhada.

Não é verdade que todos os tipos indutivos são numeráveis. Por exemplo, o tipo indutivo

Inductive cow := 
   | nose : cow
   | horn : (nat -> cow) -> cow.

não é numerável, pois, dada qualquer sequência c : nat -> cowque possamos formar, horn cque não esteja na sequência por fundamentos do gado. Se você deseja uma declaração correta do formulário "todos os tipos indutivos são contáveis", é necessário limitar severamente as construções permitidas.

Os números reais não podem ser facilmente construídos como um tipo indutivo, exceto que, na teoria dos tipos de homotopia, eles podem ser construídos como um tipo indutivo-indutivo superior , consulte o Capítulo 11 do livro HoTT . Pode-se argumentar que isso é trapaça.

Há várias definições construtivas e construções dos reais, contrariamente à alegação de Gilles. Eles podem ser amplamente divididos em duas classes:

1. Construções do tipo Cauchy nas quais os reais são vistos como uma conclusão métrica dos números racionais. Esse tipo de construção geralmente requer quocientes, embora seja possível se safar de uma definição coiundutiva, dependendo de como se trata a igualdade. Uma construção ingênua normalmente também requer opções contáveis, mas Fred Richman deu um procedimento de conclusão que funciona construtivamente sem escolha, veja seus números reais e outras conclusões .

2. $\lambda$$\Sigma$

No lado da implementação, temos várias formalizações construtivas de reais (mas não a que é horrível na biblioteca padrão Coq), por exemplo, reais reais eficientes e eficientes certificados por Robbert Krebbers e Bas Spitters Computer na Coq .

Para uma implementação real de números reais exatos, aponto-lhe o iRRAM de Norbert Müller .

$\mathbb{N} \to \mathbb{N}$