¿Definiciones constructivas estándar de enteros, racionales y reales?

10

Los números naturales se definen inductivamente como (usando la sintaxis de Coq como ejemplo)

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

¿Existe una forma estándar de definir enteros (y tal vez otros conjuntos como racionales y reales) de manera constructiva?

Alex
fuente
1
¿Qué es la definición constructiva?
Trismegistos

Respuestas:

11

Hay varias formas de definir una estructura matemática, según las propiedades que considere la definición. Entre las caracterizaciones equivalentes, cuál toma para ser la definición y cuál toma para ser una caracterización alternativa no es importante.

En matemáticas constructivas, es preferible elegir una definición que facilite el razonamiento constructivo. Para los números naturales, la forma básica de razonamiento es la inducción, lo que hace que la definición tradicional de cero o sucesor sea muy adecuada. Otros conjuntos de números no tienen esa preferencia.

Al razonar sobre cocientes, en entornos no constructivos, es común decir "elegir un miembro de la clase de equivalencia". En un entorno constructivo, es necesario describir cómo elegir un miembro. Esto facilita el ir con definiciones que construyen un objeto para cada miembro del tipo, en lugar de construir clases de equivalencia.

Z

Z:=N2/{((x,y),(x,y))x+y=x+y}
Si bien esto tiene un sentimiento ordenado (no "esto o aquello"), para el razonamiento constructivo, es más simple si la igualdad de objetos coincide con la igualdad de representaciones, por lo que podríamos definir los enteros relativos como un número natural o negativo de un número natural menos uno:
Inductive Z1 :=
  | Nonnegative : nat -> Z1   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Negative : nat -> Z1.     (* ⟦Negative x⟧ = -⟦x⟧-1 *)

Sin embargo, esta definición es extrañamente asimétrica, lo que puede hacer preferible admitir dos representaciones diferentes para cero:

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

O podemos construir los enteros relativos sin usar los naturales como un bloque de construcción:

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⟧ *)

La biblioteca estándar de Coq usa otra definición más: construye enteros positivos a partir de su notación es la base 2, ya que el dígito 1 seguido de una secuencia de dígitos 0 o 1. Luego construye Zcomo Z3desde Pos3arriba. Esta definición también tiene una representación única para cada número entero. La elección de usar la notación binaria no es para un razonamiento más fácil, sino para producir un código más eficiente cuando los programas se extraen de las pruebas.

La facilidad de razonamiento es una motivación para elegir una definición, pero nunca es un factor insuperable. Si alguna construcción hace que una prueba en particular sea más fácil, uno puede usar esa definición en esa prueba en particular y demostrar que la construcción es equivalente a la otra construcción que se eligió como definición originalmente.

NQN×N=?=Q

Los números reales son una caldera de peces completamente diferente porque no son construibles. Es imposible definir los números reales como un tipo inductivo (todos los tipos inductivos son numerables). En cambio, cualquier definición de los números reales tiene que ser axiomática, es decir, no constructiva. Es posible construir subconjuntos numerables de los números reales; la forma de hacerlo depende del subconjunto que desee construir.

Gilles 'SO- deja de ser malvado'
fuente
1
Los números reales computables parecen ser el candidato más razonable, ya que la mayoría de los usos de los números reales están vinculados a su ordenamiento habitual de alguna manera.
dfeuer
55
¿Qué significa "constructible"? Solo conozco los "conjuntos construibles" a la teoría de conjuntos, pero eso es lo que quieres decir ahora. Además, si bien es cierto que los reales son una caldera de peces completamente diferente, no es cierto que "cualquier definición de los números reales tenga que ser axiomática, es decir, no constructiva". Y en la teoría del tipo de homotopía hay una definición inductiva-inductiva más alta de los reales.
Andrej Bauer
14

La respuesta de Gilles es buena, excepto por el párrafo sobre los números reales, que es completamente falso, excepto por el hecho de que los números reales son de hecho un caldero diferente de peces. Debido a que este tipo de información errónea parece estar bastante extendido, me gustaría registrar aquí una refutación detallada.

No es cierto que todos los tipos inductivos sean numerables. Por ejemplo, el tipo inductivo

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

no es numerable, porque dada cualquier secuencia c : nat -> cowque podamos formar horn cque no esté en la secuencia por la buena base del ganado. Si desea una declaración correcta de la forma "todos los tipos inductivos son contables", debe limitar severamente las construcciones permitidas.

Los números reales no pueden construirse fácilmente como un tipo inductivo, excepto que en la teoría del tipo de homotopía pueden construirse como un tipo inductivo-inductivo superior , véase el Capítulo 11 del libro HoTT . Se podría argumentar que esto es trampa.

Hay una serie de definiciones constructivas y construcciones de los reales, en contra de lo que afirma Gilles. Se pueden dividir ampliamente en dos clases:

  1. Construcciones de tipo Cauchy en las que los reales son vistos como una terminación métrica de los números racionales. Este tipo de construcción a menudo requiere cocientes, aunque uno puede ser capaz de salirse con la suya, dependiendo de cómo se trate la igualdad. Una construcción ingenua generalmente también requiere una elección contable, pero Fred Richman dio un procedimiento de finalización que funciona de manera constructiva sin elección, vea sus números reales y otras terminaciones .

  2. λΣ

En el lado de la implementación, tenemos varias formalizaciones constructivas de reales (pero no la de la biblioteca estándar de Coq que es simplemente horrible), por ejemplo, reales exactos eficientes certificados por computadora de Robbert Krebbers y Bas Spitters .

Para una implementación real de números reales exactos , le indico el iRRAM de Norbert Müller .

NN

Andrej Bauer
fuente
Se podría suponer que axiomatizar la teoría de campos cerrados reales en Coq ...
seudónimo
Sí, podrías, y Cyril Cohen lo hizo, ver hal.inria.fr/hal-00671809v1/document . ¿Cuál es tu punto?
Andrej Bauer
No tengo razón, era solo una presunción.
Seudónimo