Как связаны языки программирования и основы математики?

В основном я знаю о трех основах математики

1. Теория множеств
2. Теория типов
3. Теория категорий

Итак, каким образом связаны языки программирования и основы математики?

РЕДАКТИРОВАТЬ

Первоначальный вопрос был «Языки программирования на основе основ математики»

с добавленным парагарфом

И реализации теории
1. Теория типов в Coq
2. Теория множеств в SETL
3. Теория категорий в Haskell

По предложению это было изменено на «Как связаны языки программирования и основы математики»

Поскольку это один из тех вопросов, в которых я недостаточно знал о том, что спрашиваю, но хотел что-то узнать, я модифицирую вопрос, чтобы сделать его более ценным для обучения и других, оставив детали, чтобы не Текущий ответ Андрея Бауэра кажется не по теме.

Спасибо за все комментарии и ответ, я учусь на них.

[Примечание: этот параграф теперь устарел.] Название вашего вопроса содержит необоснованное предположение, а именно, что языки программирования «основаны на основах математики». Как правило, это не так, хотя эти две области имеют важные отношения. Более точным утверждением было бы то, что (некоторые) языки программирования были разработаны с использованием основополагающих методов. Лучше задать вопрос: «Как связаны языки программирования и основы математики?»

Самая общая связь воплощена в лозунге « доказательства как программы» , который можно заставить работать несколькими способами. Соответствие Карри-Говарда является наиболее очевидным. С этим мы связываем сразу теорию типов, логику и программирование. Но следует подчеркнуть, что соответствие Карри-Ховарда не очень хорошо работает при наличии общей рекурсии (потому что каждый тип становится обитаемым), которую поддерживает каждый язык программирования общего назначения.

Более тонкий способ заставить лозунг работать как программы - использовать реализуемость . Здесь также мы связываем доказательства и программы, но теперь направление идет от доказательств к программам: каждое доказательство дает программу, но не каждая программа обязательно является доказательством.

Основным примером языка программирования, основанного на фундаменте, является Agda , который просто представляет собой реализацию теории зависимых типов. Однако Agda не является языком программирования общего назначения, поскольку он не поддерживает общую рекурсию. Каждая функция в Agda является полной, и есть вычислимые функции, которые не могут быть реализованы в Agda. На практике программисты не заметят этого, но заметят, что Agda не допускает неопределенные значения, например бесконечные циклы.

Coq - это не язык программирования, а скорее помощник по проверке. Тем не менее, он также имеет возможности извлечения, которые дают программы из доказательств. Корректоры и языки программирования не следует путать друг с другом.

Мы не должны забывать, что пролог и другие языки логического программирования черпают вдохновение из идеи, что вычисления - это поиск доказательства . Это, конечно, тесно связано с логикой.

Haskell - это язык программирования общего назначения, основанный на теории предметной области . То есть его семантика является теоретико-предметной, поскольку она должна учитывать частичные функции и рекурсию. Сообщество Haskell разработало ряд методов, основанных на теории категорий, из которых монады наиболее известны, но их не следует путать с монадами . В более широком смысле, расширенные функции программирования обычно обрабатываются комбинацией теории предметной области и теории категорий, но это не то, к чему опытный программист на Хаскелле может привыкнуть. Так называемая «синтаксическая категория» типов Haskell - это взгляд непрофессионала о том, как Haskell и теория категорий соответствуют друг другу.

Теория множеств (классическая или конструктивная), кажется, вдохновляет идеи в языке программирования в меньшей степени. Конечно, конструктивная теория множеств связана с программированием через конструктивную логику. Алекс Симпсон (Alex Simpson) дал одно важное применение теории интуиционистских множеств к языкам программирования. Но это довольно продвинутый материал, возможно, посмотрите эти слайды . Жан-Луи Кривин разработал очень интересный бренд реализуемости для классической теории множеств. Это хороший способ связать классическую теорию множеств и программирование.

Таким образом, теория языков программирования использует фундаментальные методы. Это не удивительно, поскольку мы считаем, что вычисления являются фундаментальной концепцией. Но слишком наивно говорить, что языки программирования «основаны» на определенных основах. На самом деле трихотомия основ «теория множеств - теория типов - теория категорий» - это опять же полезное наблюдение высокого уровня, которое можно сделать математически точным различными способами, но в этом нет ничего необходимого. Это историческая случайность.

это очень сложная тема, и есть много замечательных книг по этой теме, последняя называется « Туринский собор», истоки цифровой вселенной, а также « Двигатели логики», «математики» и «происхождение компьютера» .

Компьютерные языки развивались на протяжении многих десятилетий, но, верите или нет, существуют два оригинальных языка программирования, которые показывают, что математика и информатика тесно связаны между собой:

• Статья Тьюринга 1936 года о проблеме остановки . теоретическая конструкция , чтобы решить эту проблему , предложенную Гильберт на рубеже веков, проблема разрешения , т.е. автоматизированной процедуры для решения математических задач!

• Лямбда-исчисление Церкви, разработанное в то же время, до сих пор сохранилось на таких языках, как шутки и схемы

Есть две ключевые фигуры, которые пересекли границы математики и информатики в отношении «языков программирования»:

• Теория информации, впервые разработанная Шенноном, показывает глубокие связи между математикой и информатикой.

• Другой ключевой фигурой, которая пересекает математику и информатику, является фон Нейман . он изобрел архитектуру фон Неймана для хранения программ в памяти.

еще раньше "языки программирования":

• английское слово «компьютер» изначально означало нечто большее, чем «калькулятор», в котором использовались математические операции над числами, и его значение существенно сместилось в современную концепцию программирования общего назначения. поэтому существует связь между языками программирования и ранними калькуляторами.
• перфокарты, используемые в ткацких станках конца 19-го и начала 20-го века, были «языком программирования» для ткацких узоров. Обратите внимание, что перфокарты использовались для программирования мэйнфреймов в 1960-х годах. Первоначально они рассматривались как «вычислительные машины» (с использованием математики!), а не как современные компьютеры общего назначения.
• Бэббидж и Ада Лавлейс разработали элементарные ранние концепции «языков программирования» в середине 1800-х годов на «вычислительном движке»
• Булева алгебра изначально была чисто математической концепцией, изобретенной Булем
• древние (тысячелетние) счеты для математических расчетов считаются предвестником современного компьютера. но можно сказать, что операции по манипулированию им были своего рода «языком программирования» (за которым следовали люди)

тем не менее, в современных языках программирования по мере увеличения и масштабирования абстракции четкая прямая связь с математикой несколько снижалась в течение десятилетий, но она всегда будет весьма присуща и в некотором смысле усиливается. Например, такие языки, как Java, с ее строгими типами имеют связи с математикой, и в начале 1990-х годов основные компьютерные языки (например, c ++, Java, Ruby и т. д.) начали явно реализовывать многие математические объекты более высокого уровня как примитивы в такие языки, как наборы, деревья (например, Btrees или hashmaps) и т. д.