Por que naturais em vez de números inteiros?

28

Estou interessado em saber por que os números naturais são tão amados pelos autores de livros sobre teoria das linguagens de programação e teoria dos tipos (por exemplo, J. Mitchell, Fundações para linguagens de programação e B. Pierce, Tipos e linguagens de programação). A descrição do cálculo lambda de tipo simples e, em particular, a linguagem de programação PCF são geralmente baseadas em Nat e Bool. Para as pessoas que usam e ensinam PL industriais de uso geral, é muito mais natural tratar números inteiros do que naturais. Você pode mencionar algumas boas razões pelas quais o teórico de PL prefere os nat? Além disso, é um pouco menos complicado. Existem razões fundamentais ou é apenas uma honra a tradição?

UPD Por todos esses comentários sobre a “fundamentalidade” dos naturais: conheço bem todas essas coisas legais, mas prefiro ver um exemplo quando é realmente vital ter essas propriedades na teoria de tipos da teoria de PL. Por exemplo, indução amplamente mencionada. Quando temos qualquer tipo de lógica (que simplesmente digita LC é), como lógica básica de primeira ordem, usamos realmente a indução - mas a indução na árvore de derivação (que também temos no lambda).

Minha pergunta vem basicamente de pessoas da indústria, que querem ganhar alguma teoria fundamental das linguagens de programação. Eles costumavam ter números inteiros em seus programas e sem argumentos e aplicações concretas à teoria que está sendo estudada (teoria dos tipos no nosso caso). Por que estudar linguagens apenas com nat, elas se sentem bastante decepcionadas.

Artem Pelenitsyn
fonte
Acho que essa não é uma questão de nível de pesquisa, embora seja interessante.
Raphael
4
Não é, mas é uma espécie de questão geral, que aceitamos.
Suresh Venkat
1
Gostaria de saber se, de alguma forma, o conjunto de números inteiros não negativos pode ser ainda mais fundamental que os números naturais devido às propriedades exclusivas do valor 0 que não existe no último. Também gostaria de sugerir que isso é mais válida quanto a escolha do tipo numérico fundamental para computadores digitais dada a importância do 0.
Richard Cook
Eu não entendo o seu UPD . Os naturais são mais fundamentais do que números inteiros, e as respostas dão exemplos de por que esse é o caso.
Radu GRIGore
Re: UPD. Não sei ao certo por que "pessoas da indústria" ficariam "decepcionadas". (Eu mesmo passei minha carreira na indústria.) Por que alguém deveria esperar que essa teoria fosse uma extensão óbvia do que eles já estão familiarizados? É bastante comum que certas coisas comuns na indústria, como variáveis ​​inteiras, existam mais por "razões históricas" do que por profundas teorias.
Marc Hamann

Respostas:

24

Resposta curta: os naturais são os primeiros ordinais de limite. Portanto, eles desempenham um papel central na teoria axiomática dos conjuntos (por exemplo, o axioma do infinito é a afirmação que eles existem) e na lógica, e os teóricos da PL tendem a compartilhar preocupações fundamentais com os lógicos. Queremos ter acesso ao princípio da indução para provar total correção, terminação e propriedades semelhantes, e os naturais são uma (er) escolha natural de ordem bem-vinda.

Não quero sugerir que números inteiros binários de largura finita sejam objetos menos interessantes. Eles são representações dos p-adics e nos permitem usar métodos de séries de poder na teoria dos números e na combinatória. Isso significa que seu significado se torna mais visível nos algoritmos do que no PL, pois é quando começamos a nos preocupar mais com a complexidade do que com a terminação.

Neel Krishnaswami
fonte
20

Os naturais são um conceito muito mais fundamental que os números inteiros.

A indução ocorre sobre os naturais e os números inteiros podem ser derivados dos naturais com a simples adição de um operador inverso unário.

Eu realmente gostaria de fazer a pergunta inversa: por que os projetistas da linguagem de programação inicial (e da máquina de registro) consagraram números inteiros como o tipo de dados básico quando são tão secundários e tão facilmente derivados de naturais?

Eu suspeito que é apenas porque havia algumas codificações binárias legais que podiam lidar com números inteiros elegantemente. ;-)

Pense com que frequência você deseja ignorar o intervalo negativo de um número inteiro programático e considere o impulso de ter um tipo inteiro não assinado para recuperar o bit perdido.

Marc Hamann
fonte
5
Outro motivo: se você quiser algo como números da Igreja, um número inteiro negativo teria que indicar inversão de função. Portanto, nesse contexto, os números inteiros seriam mais naturais em um cálculo de funções bijetivas computacionalmente.
Por Vognsen
@ Per Vognsen: não tenho certeza de que maneira você está discutindo lá. Mas acho seguro dizer que as funções bijetivas computáveis ​​são menos fundamentais do que as funções computáveis ​​arbitrárias na maioria das vezes. ;-)
Marc Hamann
Não há dúvida de que números complexos, que estão no topo da hierarquia de números Números Naturais -> Inteiros -> Números Racionais -> Números Reais -> Números Complexos são mais fundamentais que os outros, porque possuem propriedades algébricas "mais agradáveis". Eles estão em toda parte na ciência, mas estão visivelmente ausentes nos "fundamentos" da matemática. Portanto, a resposta para números inteiros ou naturais mais "fundamentais" depende realmente de quem você pergunta: algoritmista ou algébrico.
Tegiri Nenashi
Como este é um site da TCS, acho que estamos seguros em privilegiar a visão da ciência da computação. ;-) Computacionalmente, essa hierarquia é progressiva: cada nova entrada é literalmente construída sobre a anterior. Como "fundamental" geralmente se refere a algo na base, acho que o fim natural é o caminho certo para conferir esse título.
Marc Hamann
17

NZ

NZ

Rafael
fonte
11

Ainda outro motivo (relacionado aos já dados, mas essa resposta acrescenta novas informações) é que existe uma construção muito simples e natural de quocientes, que acompanha um bom princípio de indução [como já foi dito] . O que não foi expandido é o quão difícil é criar uma construção sem números de quocientes.

Quanto mais programação eu faço onde quero alta segurança, mais preciso do natural e acho que ter apenas os números inteiros predefinidos para mim é uma verdadeira dor.

Jacques Carette
fonte
Existem idiomas que têm um tipo básico de naturais, você sabe.
Raphael
@Raphael: eu sei. Mas não os que eu gosto de outra maneira (ou seja, Haskell e OCaml). Não estou pronto para iniciar a 'programação' na Agda ou na Coq.
precisa
O que há de tão ruim nos quocientes?
David Harris
3
Os quocientes são ótimos na semântica. Eles são muito, muito mais difíceis de lidar em cálculos reais e em representações concretas. Existem inúmeros trabalhos sobre como lidar com eles em Coq, Isabelle, Agda (teoria dos tipos em geral) etc. Eu apenas assumi que era o conhecimento do folclore em todas as comunidades que os quocientes são apenas uma dor para lidar 'na realidade'.
precisa
2
Sinto que esta é a resposta mais forte do grupo: os naturais são o tipo de dados indutivo não trivial mais simples. depois de definir e provar propriedades simples para números naturais, você abre caminho para tipos de dados indutivos mais complexos, como listas ou árvores.
Cody
7

Existem boas razões pelas quais os teóricos da PL preferem naturais em vez de números inteiros? Existem alguns, mas em um livro de texto sobre semântica da linguagem de programação, acho que não há razão técnica para isso. Não consigo pensar em nenhum outro lugar além de sistemas de tipo dependente, onde a indução de dados é importante na teoria do PL. Outros livros de Mike Gordon , David Schmidt , Bob Tennent e John Reynolds não o fazem. (E esses livros provavelmente seriam muito mais adequados para ensinar pessoas que se preocupam com PLs de uso geral!)

Então, você tem a prova de que isso não é necessário. De fato, eu diria que um bom livro de teoria da PL deve ser paramétrico nos tipos primitivos da linguagem de programação, e é enganoso sugerir o contrário.

Uday Reddy
fonte
6

Os naturais e os bools e as operações com eles podem ser codificados no cálculo lambda puro de maneira direta, como os chamados números da Igreja (e os bools da igreja, eu acho). Não está claro como alguém codificaria números inteiros, embora isso possa obviamente ser feito.

Dave Clarke
fonte
Eu quis dizer antes de tudo o cálculo lambda digitado. O curso dos livros que mencionei no post principal é baseado nisso. Eu acho que lambda não tipificado não é tão vital na teoria dos tipos e na teoria de PL atualmente (posso estar errado, mas é o que vejo nesses livros). De qualquer forma, obrigado!
Artem Pelenitsyn