¿Por qué los naturales en lugar de los enteros?

28

Me interesa saber por qué los autores de libros sobre teoría de los lenguajes de programación y teoría de los tipos adoran los números naturales (por ejemplo, J. Mitchell, Fundamentos para los lenguajes de programación y B. Pierce, Tipos y lenguajes de programación). La descripción del cálculo lambda de tipo simple y, en particular, el lenguaje de programación PCF generalmente se basan en Nat's y Bool's. Para las personas que usan y enseñan PL industriales de uso general, es mucho más natural tratar enteros en lugar de naturales. ¿Puedes mencionar algunas buenas razones por las cuales los teóricos de PL prefieren los nat? Además de eso, es un poco menos complicado. ¿Hay alguna razón fundamental o es solo un honor a la tradición?

UPD Para todos esos comentarios sobre la "fundamentalidad" de los naturales: soy bastante consciente de todas esas cosas geniales, pero prefiero ver un ejemplo cuando es realmente vital tener esas propiedades en la teoría de tipos de la teoría de PL. Por ejemplo, la inducción ampliamente mencionada. Cuando tenemos algún tipo de lógica (que simplemente escribe LC es), como la lógica básica de primer orden, realmente utilizamos la inducción, pero la inducción en el árbol de derivación (que también tenemos en lambda).

Mi pregunta básicamente proviene de personas de la industria, que quieren obtener una teoría fundamental de los lenguajes de programación. Solían tener enteros en sus programas y sin argumentos y aplicaciones concretas a la teoría que se estaba estudiando (teoría de tipos en nuestro caso) por qué estudiar idiomas solo con nat, se sienten bastante decepcionados.

Artem Pelenitsyn
fuente
Supongo que esta no es una pregunta de nivel de investigación, aunque sí interesante.
Raphael
44
No lo es, pero es una especie de pregunta global que aceptamos.
Suresh Venkat
1
Me pregunto si de alguna manera el conjunto de enteros no negativos podría ser aún más fundamental que los números naturales debido a las propiedades únicas del valor 0 que no existe en este último. También sugeriría que esto es más válido como la elección del tipo numérico fundamental para las computadoras digitales dada la importancia de 0.
Richard Cook
No entiendo tu UPD . Los naturales son más fundamentales que los enteros, y las respuestas dan ejemplos de por qué este es el caso.
Radu GRIGore
Re: UPD. No estoy muy seguro de por qué la "gente de la industria" estaría "decepcionada". (He pasado mi carrera en la industria yo mismo). ¿Por qué alguien debería esperar que la teoría sea una extensión obvia de lo que ya están familiarizados? Es bastante común que ciertas cosas comunes en la industria, como las variables enteras, existan más por "razones históricas" que por razones teóricas profundas.
Marc Hamann

Respuestas:

24

Respuesta corta: los naturales son los ordinales de primer límite. Por lo tanto, juegan un papel central en la teoría de conjuntos axiomáticos (por ejemplo, el axioma del infinito es la afirmación de que existen) y la lógica, y los teóricos de PL tienden a compartir preocupaciones fundamentales con los lógicos. Queremos tener acceso al principio de inducción para probar la corrección total, la terminación y propiedades similares, y los productos naturales son una (er) elección natural de buen orden.

Sin embargo, no quiero implicar que los enteros binarios de ancho finito sean objetos menos interesantes. Son representaciones de los p-adics y nos permiten usar métodos de series de potencia en teoría de números y combinatoria. Esto significa que su importancia se hace más visible en algoritmos que PL, ya que es cuando comenzamos a preocuparnos más por la complejidad que por la terminación.

Neel Krishnaswami
fuente
20

Los naturales son un concepto mucho más fundamental que los enteros.

La inducción ocurre sobre los naturales y los enteros pueden derivarse de los naturales con la simple adición de un operador inverso unario.

Realmente me gustaría hacer la pregunta inversa: ¿por qué los primeros diseñadores de lenguaje de programación (y máquina de registro) consagraron los enteros como el tipo de datos básico cuando son tan secundarios y se derivan tan fácilmente de los naturales?

Sospecho que es solo porque había algunas codificaciones binarias geniales que podían manejar enteros con elegancia. ;-)

Piense con qué frecuencia desea ignorar el rango negativo de un entero programático y considere el impulso de tener un tipo entero sin signo para recuperar el bit perdido.

Marc Hamann
fuente
55
Otra razón: si desea algo como los números de la Iglesia, un entero negativo tendría que denotar la inversión de la función. Entonces, en ese contexto, los enteros serían más naturales en un cálculo de funciones biyectivas computables.
Por Vognsen
@Per Vognsen: no estoy seguro de qué manera está discutiendo allí. Pero creo que es seguro decir que la mayoría de las veces las funciones biyectivas computables son menos fundamentales que las funciones computables arbitrarias. ;-)
Marc Hamann
No hay duda de que los números complejos, que están en la parte superior de la jerarquía numérica Números naturales -> Números enteros -> Números racionales -> Números reales -> Números complejos son más fundamentales que los demás, porque tienen propiedades algebraicas "más agradables". Están en todas partes en la ciencia, pero están notablemente ausentes en los "fundamentos" de las matemáticas. Entonces, la respuesta a los enteros más "fundamentales" o naturales realmente depende de a quién le pregunte: algoritmo o algebraista.
Tegiri Nenashi
Dado que este es un sitio de TCS, creo que estamos seguros de privilegiar la visión de la informática. ;-) Computacionalmente, esa jerarquía es progresiva: cada nueva entrada está literalmente construida sobre la anterior. Como "fundamental" generalmente se refiere a algo en la base, creo que el final natural es el adecuado para conferir ese título.
Marc Hamann el
17

NZ

NZ

Rafael
fuente
11

Otra razón (relacionada con las que ya se dieron, pero esta respuesta agrega nueva información) es que hay una construcción muy simple y sin cocientes de los naturales, que viene junto con un buen principio de inducción [como ya se ha dicho] . Lo que no se ha ampliado es lo difícil que es llegar a una construcción de enteros sin cocientes.

Cuanto más programación hago donde quiero mayor seguridad, más necesito los naturales, y encuentro que tener solo los enteros predefinidos para mí es un verdadero dolor.

Jacques Carette
fuente
Hay idiomas que tienen un tipo básico para los naturales, ya sabes.
Raphael el
@Raphael: lo sé. Pero no los que me gustan (es decir, Haskell y OCaml). No estoy listo para comenzar a 'programar' en Agda o Coq.
Jacques Carette
¿Qué tienen de malo los cocientes?
David Harris el
3
Los cocientes son geniales en la semántica. Son mucho, mucho más difíciles de tratar en los cálculos reales y en las representaciones concretas. Hay innumerables documentos sobre cómo tratarlos en Coq, Isabelle, Agda, (teoría de tipos en general), etc. Simplemente asumí que era conocimiento del folclore en todas las comunidades que los cocientes son simplemente difíciles de manejar 'en realidad'.
Jacques Carette
2
Siento que esta es la respuesta más fuerte del grupo: los naturales son el tipo de datos inductivo no trivial más simple. Una vez que haya dado definición y demostrado propiedades simples para los números naturales, ha allanado el camino para tipos de datos inductivos más complejos, como listas o árboles.
cody
7

¿Hay alguna buena razón por la cual los teóricos de PL prefieren los naturales en lugar de los enteros? Hay algunos, pero en un libro de texto sobre semántica del lenguaje de programación, creo que no hay una razón técnica por la que lo necesiten. No puedo pensar en otro lugar que no sean los sistemas de tipo dependiente, donde la inducción de datos es importante en la teoría PL. Otros libros de texto de Mike Gordon , David Schmidt , Bob Tennent y John Reynolds no lo hacen. (¡Y esos libros probablemente serían mucho más adecuados para enseñar a las personas que se preocupan por los PL industriales de uso general!)

Así que, ahí, se tiene la prueba de que es no es necesario. De hecho, afirmaría que un buen libro de texto de teoría PL debería ser paramétrico en los tipos primitivos del lenguaje de programación, y es engañoso sugerir lo contrario.

Uday Reddy
fuente
6

Los productos naturales y los bools y las operaciones en ellos se pueden codificar en el cálculo lambda puro de una manera directa, como los llamados números de la Iglesia (y los bools de la Iglesia, supongo). No está claro cómo se codificarían bien los enteros, aunque obviamente se puede hacer.

Dave Clarke
fuente
Me refería en primer lugar al cálculo lambda escrito. El curso de los libros que mencioné en la publicación principal se basa en ello. Supongo que el lambda sin tipo no es tan vital en la teoría de tipos y la teoría de PL hoy en día (puedo estar equivocado, pero eso es lo que veo en esos libros). ¡Gracias de todas formas!
Artem Pelenitsyn