Незадолго до появления реального программирования ряд математиков уже начал мечтать о нём. И фантазировать, как оно могло бы быть устроено
( Read more... )
Можно прямо сразу взять сабжевую книжку Пенроуза - там чуть ли не половина текста такая. А можно немного подождать - где-то к среде должны выложить статью про «диагональный аргумент» Кантора. Про Гёделя ждать придётся дольше - там слишком много ошибок. Я уже 80 страниц написал и надо ещё минимум столько же.
Разве что про Тьюринга я не готов - это примерно как анализ рассуждений о закономерностях языка Brainfuck писать.
Иначе говоря: написать несколько экранов текста с фантазиями про автомобилистов-теоретиков - это легко, а указать конкретный пример - "идите ищите сами, мне некогда"?)
Так существует же “математика для программистов”, рефлексирующая разную алгоритмику (с некоторой ориентацией на императивный подход). Те же Кнут, Дийкстра, Хоар. Не считая кучи полезных прикладных вещей из алгебры, комбинаторики и т.д. Поэтому не совсем понятно, почему Вы выбрали сугубо теоретические построения, касающиеся вычислимости, а потом грустите, что они плохо подходят для описания алгоритмов. Микроскоп и гвозди 😀
Кнут уже на основе приложений теоретизировал. То есть были работоспособные генераторы случайных чисел или сортировки, поиск, которые стоило усовершенствовать. Он это, возможно (может ведь статься, что не он), сделал. Усовершенствовал. Но его язык из его построений выбрасывают первым делом.
Выходит, что его язык, в отличие от некоторых (не всех!) особенностей его алгоритмов, имел сугубо субъективную ценность. Не только язык, но и код его ни к чему, я лучше писал.
Можете прояснить тогда, в каком месте Вы видите разрыв именно по алгоритмам?
Ведь если брать того же Кнута, то в 3х-томнике он использовал псевдоязык только для того, чтобы показать, как оно ложится на реальный код на императивном ЯП и оценивать разные аспекты алгоримов. Это его книга для программистов. Для математиков он написал Конкретную математику. Доказательствам корректности программ (формальные спецификации и иже с ними) тоже уже под полтинник, Дисциплина программирования Дийкстры была настольной книгой у многих.
Возможно, есть какие-то неохваченные области, но сходу их не припомню.
Насколько я понимаю вся идея с Тьюринг-машиной не в том чтобы на ней что-либо запускать, а использовать её в качестве простой математической модели, и потом просто строить изоморфизм между ТМ и реальными процессорами/байткодом и т.д. Т.е. можно было бы в принципе не полениться и доказать что есть такие функции на условной Scala, для которых невозможно определить войдет ли она в бесконечный цикл - но вместо этого можно доказать что (упрощенно): 1. код Скалы компилируется на JVM 2. интерпретатор байткода JVM (опять же, упрощенно) эквивалентен машине Тьюринга 3. а для машины Тьюринга мы уже знаем про halting problem Таким образом мы уже сразу же знаем что для кода и на Scala, и на Kotlin, и на Clojure, и на собственно Яве существует halting problem. Т.е. это абстракция, которая позволяет ленивым программистам - а программист должен быть ленив - без особых усилий рассуждать о возможностях языка, что может быть весьма и весьма полезно при написании DSL и т.д.
Любой нормальный язык программирования лучше подходит для рассуждений о языках программирования, чем машина Тьюринга. И его закономерности гораздо проще переносить на другие языки программирования.
Это чепуха, конечно. Реальные языки программирования слишком сложны синтаксически, чтобы было возможно строго о них рассуждать. Но каждый из них сводится к языку МТ, который чрезвычайно прост синтаксически и который, как уже отметили выше, служит прекрасной математической моделью.
Но самая чепуха в том, что в двадцать первом веке кто-то всё ещё думает, что «синтаксическая простота» = «простоте анализа» = «простоте использования».
Хотя вроде бы каждый из них давно мог бы попробовать позаниматься математикой при помощи системы обозначений аксиоматики Пеано и быстро понять на собственном примере, что «S(S(S(S(1))))» хотя и выигрывает в «синтаксической простоте» перед позиционной записью чисел, поскольку не содержит этой самой позиционной записи, тем не менее, совсем не проще записи «5». А если в этом вдруг ещё останутся сомнения, то этот человек всё ещё может записать, например, 521 + 32 в аксиоматике Пеано и попробовать глазами проверить, не допустил ли он в этой записи какую-то ошибку.
Не, ну реал, двадцать первый век на дворе, а кто-то всё ещё думает, что «меньше команд» = «проще язык».
Есть мнение, что ограничивать бред математиков не плодотворно, пока они сами плодотворны. Математики - не самые умные люди, чему множество четких подтверждений, но умеют взглянуть на некоторые проблемы необычно.
Comments 68
Так и хочется спросить: а можно конкретный пример рассуждений и выводов данных математиков?
Reply
Разве что про Тьюринга я не готов - это примерно как анализ рассуждений о закономерностях языка Brainfuck писать.
Reply
Reply
Вы не согласны?
Как только эта абстракция так долго продержалась...
Ведь, наверное, _любая_ другая более удобна для почти любых применений.
Reply
Reply
Выходит, что его язык, в отличие от некоторых (не всех!) особенностей его алгоритмов, имел сугубо субъективную ценность. Не только язык, но и код его ни к чему, я лучше писал.
Reply
Ведь если брать того же Кнута, то в 3х-томнике он использовал псевдоязык только для того, чтобы показать, как оно ложится на реальный код на императивном ЯП и оценивать разные аспекты алгоримов. Это его книга для программистов. Для математиков он написал Конкретную математику. Доказательствам корректности программ (формальные спецификации и иже с ними) тоже уже под полтинник, Дисциплина программирования Дийкстры была настольной книгой у многих.
Возможно, есть какие-то неохваченные области, но сходу их не припомню.
Reply
Дейкстра как раз называл себя «программистом» - одним из первых в мире начал.
Reply
Reply
Т.е. можно было бы в принципе не полениться и доказать что есть такие функции на условной Scala, для которых невозможно определить войдет ли она в бесконечный цикл - но вместо этого можно доказать что (упрощенно):
1. код Скалы компилируется на JVM
2. интерпретатор байткода JVM (опять же, упрощенно) эквивалентен машине Тьюринга
3. а для машины Тьюринга мы уже знаем про halting problem
Таким образом мы уже сразу же знаем что для кода и на Scala, и на Kotlin, и на Clojure, и на собственно Яве существует halting problem.
Т.е. это абстракция, которая позволяет ленивым программистам - а программист должен быть ленив - без особых усилий рассуждать о возможностях языка, что может быть весьма и весьма полезно при написании DSL и т.д.
Reply
Reply
Реальные языки программирования слишком сложны синтаксически, чтобы было возможно строго о них рассуждать.
Но каждый из них сводится к языку МТ, который чрезвычайно прост синтаксически и который, как уже отметили выше, служит прекрасной математической моделью.
Reply
Хотя вроде бы каждый из них давно мог бы попробовать позаниматься математикой при помощи системы обозначений аксиоматики Пеано и быстро понять на собственном примере, что «S(S(S(S(1))))» хотя и выигрывает в «синтаксической простоте» перед позиционной записью чисел, поскольку не содержит этой самой позиционной записи, тем не менее, совсем не проще записи «5». А если в этом вдруг ещё останутся сомнения, то этот человек всё ещё может записать, например, 521 + 32 в аксиоматике Пеано и попробовать глазами проверить, не допустил ли он в этой записи какую-то ошибку.
Не, ну реал, двадцать первый век на дворе, а кто-то всё ещё думает, что «меньше команд» = «проще язык».
Reply
Reply
Leave a comment