Почему натуральные числа вместо целых?

28

Меня интересует, почему натуральные числа так любимы авторами книг по теории языков программирования и теории типов (например, Дж. Митчелл, Основы языков программирования и Б. Пирс, Типы и языки программирования). Описание простейшего лямбда-исчисления и, в частности, языка программирования PCF обычно основано на принципах Ната и Була. Для людей, использующих и обучающих промышленным PL общего назначения, гораздо более естественно рассматривать целые числа, а не натуральные. Можете ли вы назвать несколько веских причин, почему теоретик ЛП предпочитает нац? Кроме того, это немного менее сложно. Есть ли фундаментальные причины или это просто честь традиции?

UPD Для всех этих комментариев об «фундаментальности» натуралов: я хорошо осведомлен обо всех этих классных вещах, но я бы предпочел увидеть пример, когда действительно важно иметь эти свойства в теории типов теории PL. Например, широко упоминается индукция. Когда у нас есть какая-либо логика (которая просто типизирована как LC), как и базовая логика первого порядка, мы действительно используем индукцию - но индукцию по дереву деривации (которое мы также имеем в лямбде)

Мой вопрос в основном исходит от людей из промышленности, которые хотят получить фундаментальную теорию языков программирования. Раньше у них были целые числа в своих программах, и без конкретных аргументов и приложений к изучаемой теории (в нашем случае, к теории типов), почему для изучения языков только с натами они чувствуют себя довольно разочарованными.

Артем Пеленицын
источник
Я думаю, что это не вопрос исследовательского уровня, хотя интересный.
Рафаэль
4
Это не так, но это своего рода большой вопрос, который мы принимаем.
Суреш Венкат
1
Мне интересно, если каким-то образом набор неотрицательных целых чисел может быть даже более фундаментальным, чем натуральные числа, из-за уникальных свойств 0-значения, которое не существует в последнем. Я также предположил бы, что это более справедливо в качестве выбора основного числового типа для цифровых компьютеров, учитывая важность 0.
Ричард Кук
Я не понимаю вашего UPD . Naturals являются более фундаментальными, чем целые числа, и ответы дают примеры того, почему это так.
Раду GRIGore
Re: UPD. Я не слишком уверен, почему "люди из промышленности" будут "разочарованы". (Я провел свою карьеру в промышленности сам.) Почему кто-то должен ожидать, что теория должна стать очевидным продолжением того, с чем они уже знакомы? Весьма распространено, что некоторые общие для промышленности вещи, такие как целочисленные переменные, существуют больше по «историческим причинам», чем по глубоким теоретическим.
Марк Хаманн

Ответы:

24

Краткий ответ: натуральные числа - это первые предельные порядковые числа. Следовательно, они играют центральную роль в аксиоматической теории множеств (например, аксиома бесконечности - это утверждение, что они существуют) и в логике, и теоретики PL имеют тенденцию делиться фундаментальными заботами с логиками. Мы хотим иметь доступ к принципу индукции, чтобы доказать полную правильность, завершение и подобные свойства, и натуральные вещества - это естественный выбор порядка.

Я не хочу подразумевать, что двоичные целые числа конечной ширины - все же менее интересные объекты. Они являются представлениями p-adics и позволяют нам использовать методы степенных рядов в теории чисел и комбинаторике. Это означает, что их значение становится более заметным в алгоритмах, чем в PL, поскольку именно тогда мы начинаем больше заботиться о сложности, а не об окончании.

Нил Кришнасвами
источник
20

Naturals - гораздо более фундаментальная концепция, чем целые числа.

Индукция происходит над натуральными числами, а целые числа могут быть получены из натуральных чисел с простым добавлением унарного обратного оператора.

Я бы на самом деле хотел задать обратный вопрос: почему ранние разработчики языка программирования (и регистрации машин) закрепляли целые числа в качестве основного типа данных, когда они настолько вторичны и так легко получены из натуральных чисел?

Я подозреваю, что это только потому, что были некоторые классные двоичные кодировки, которые могли элегантно обрабатывать целые числа. ;-)

Подумайте, как часто вы хотите игнорировать отрицательный диапазон целочисленного значения в программе, и учтите, что импульс имеет целочисленный тип без знака для восстановления потерянного бита.

Марк Хаманн
источник
5
Другая причина: если вы хотите что-то вроде церковных цифр, отрицательное целое число должно будет обозначать инверсию функции. Таким образом, в этом контексте целые числа были бы более естественными в исчислении вычислимо биективных функций.
За Вогсен
@Per Vognsen: не уверен, каким образом вы спорите там. Но я думаю, что можно с уверенностью сказать, что вычислимые биективные функции в большинстве случаев менее фундаментальны, чем произвольные вычислимые функции. ;-)
Марк Хаманн
Нет сомнений в том, что комплексные числа, которые находятся на вершине иерархии чисел Естественные числа -> Целые числа -> Рациональные числа -> Вещественные числа -> Комплексные числа, являются более фундаментальными, чем другие, потому что они имеют "более хорошие" алгебраические свойства. Они повсюду в науке, но явно отсутствуют в «основах» математики. Таким образом, ответ на то, что является более «фундаментальными» целыми числами или натуральными числами, действительно зависит от того, кого вы спрашиваете: алгоритмист или алгебраист.
Тегири Ненаши
Поскольку это сайт TCS, я думаю, что мы в безопасности, предоставляя привилегию взгляду на информатику. ;-) В вычислительном отношении эта иерархия является прогрессивной: каждая новая запись буквально построена на предыдущей. Поскольку «фундаментальный» обычно относится к чему-то в основании, я думаю, что естественный конец - это то, что нужно для присвоения этого титула.
Марк Хаманн
17

NZ

NZ

Рафаэль
источник
11

Еще одна причина (связанная с уже приведенными, но этот ответ добавляет новую информацию) заключается в том, что существует очень простая конструкция без натуральных факторов, которая сопровождается хорошим принципом индукции [как уже было сказано] , Что не было расширено, так это то, как трудно придумать конструкцию целых чисел без фактора.

Чем больше я занимаюсь программированием там, где мне нужна высокая степень уверенности, тем больше мне нужны натуралы, и я считаю, что иметь только целые числа, заранее определенные для меня, настоящая боль.

Жак Каретт
источник
Знаете, есть языки, которые имеют базовый тип для натуралов.
Рафаэль
@ Рафаэль: я знаю. Но не те, которые мне нравятся (а именно Haskell и OCaml). Я не совсем готов начать «программирование» в Agda или Coq.
Жак Каретт
Что такого плохого в коэффициентах?
Дэвид Харрис
3
Коэффициенты велики в семантике. С ними гораздо сложнее иметь дело в реальных вычислениях и в конкретных представлениях. Существует бесчисленное множество статей о том, как с ними справляться, в Coq, Isabelle, Agda (теория типов в целом) и т. Д. Я просто предположил, что во всех сообществах фольклорным знанием является то, что с коэффициентами просто трудно иметь дело «в реальности».
Жак Каретт
2
Я чувствую, что это самый сильный ответ из этой группы: Naturals - самый простой нетривиальный индуктивный тип данных. как только вы дали определение и доказали простые свойства для натуральных чисел, вы проложили путь к более сложным индуктивным типам данных, таким как списки или деревья.
Коди
7

Есть ли веские причины, по которым теоретики PL предпочитают натуральные числа вместо целых? Есть некоторые, но в учебнике по семантике языка программирования, я думаю, нет технической причины, по которой они нужны. Я не могу думать ни о каком другом месте, кроме систем зависимого типа, где индукция данных важна в теории PL. Другие учебники Майка Гордона , Дэвида Шмидта , Боба Теннента и Джона Рейнольдса этого не делают. (И эти книги, вероятно, были бы намного более подходящими для обучения людей, которые заботятся о промышленных PL общего назначения!)

Итак, у вас есть доказательство того, что в этом нет необходимости. Фактически, я бы сказал, что хороший учебник по теории PL должен быть параметрическим в примитивных типах языка программирования, и было бы неверно предлагать иное.

Удай Редди
источник
6

Природные и логические выражения и операции над ними могут быть прямо и просто закодированы в чистом лямбда-исчислении, как так называемые церковные цифры (и, я полагаю, церковные числа). Не ясно, как можно красиво кодировать целые числа, хотя это, очевидно, можно сделать.

Дэйв Кларк
источник
Я имел в виду прежде всего набранное лямбда-исчисление. Курс книг, которые я упомянул в верхнем посте, основан на нем. Я думаю, что нетипизированная лямбда не столь важна в теории типов и теории PL в настоящее время (я могу ошибаться, но это то, что я вижу в этих книгах). В любом случае, благодарю Вас!
Артем Пеленицын