Путешествие во времени - довольно распространенный научно-фантастический сюжет, настолько распространенный, что существуют разные теории относительно того, что произойдет, если вы вернетесь назад во времени и повлияете на прошлое. Хотя путешествия во времени сделали некоторые фильмы и книги занимательными, в реальном мире они не имели большого успеха.
Теперь есть язык программирования под названием Mariposa, который утверждает, что реализует путешествие во времени как часть своего набора функций. Такие языки создаются как способ поиграть с новой или необычной функцией, такой как присвоение переменных вне обычного порядка выполнения — более просторечно, путешествие во времени.
Путешествие во времени в терминах программирования обычно означает перемещение вперед и назад по коду или извлечение предыдущих состояний, а не манипулирование реальным четырехмерным пространством-временем. Мы еще не совсем в том будущем (или находимся?). Но информатика уже давно пытается рассуждать о времени в электронных системах, благодаря постоянному интересу к параллелизму и передаче сообщений в реальном времени.
Путешествия.Назад (время.Будущее)
Mariposa позволяет вам манипулировать порядком выполнения, присваивая переменной instant , а затем устанавливая контекст этого экземпляра. Вот базовый пример, взятый из Mariposa readme:
Согласно обычному порядку операций, в этом коде должно быть выведено “1”. Но поскольку экземпляру во второй строке присваивается t, любые изменения, указанные в блоке at t:, применяются немедленно, и этот код выводит “2”. Язык ограничивает перемещение к одному и тому же экземпляру дважды и позволяет считывать и записывать значения в родительских фреймах.
С помощью некоторой цепочки и установки t = $ (now()) внутри блоков at t:, то есть изменяя текущий экземпляр в контексте перемещения во времени, вы можете создать некоторые неожиданные варианты поведения. Вопрос о том, полезно ли такое поведение для решения вычислительных задач, является предметом обсуждения — автор говорит, что они создали язык “как исследовательскую игру”. Конечно, любое приложение, построенное с учетом времени, может принести пользу, но только если есть необходимость манипулировать историческими значениями в метках времени, а не просто записывать их.
Хотя в последнее время Mariposa привлекла к себе изрядное внимание, это не первая реализация путешествий во времени в программировании. Существует пакет Haskell, соответствующим образом называемый tardis, который создает два преобразователя состояния: один перемещается вперед во времени, а другой назад. Как объясняется в документации, “Самый краткий способ объяснить это так: getPast извлекает значение из последнего sendFuture, в то время как getFuture извлекает значение из следующего sendPast”. Прошлое одной функции - это будущее другой.
Программное манипулирование значениями может позволить реализовать некоторую интересную логику, или это может быть новшеством. Однако перемещение во времени при отладке кода имеет реальные преимущества и историю, восходящую, по крайней мере, к Smalltalk. Текущие фреймворки, включающие реализации отладчика перемещения во времени, включают Elm, интерфейсную систему на основе функционального программирования, и Redux, контейнер состояний для приложений JavaScript, который использует записи журнала для воссоздания любого момента времени. Существует множество реализаций этих отладчиков для других систем, включая WinDbg (Windows), rr (Linux) и Undo (Linux).
Языки программирования с перемещением во времени изменяют значения переменных в предыдущих или будущих состояниях. Но если вы работаете с большим количеством значений, вы, вероятно, используете базу данных вместо переменных в памяти. В временных базах данных транзакции никогда не перезаписываются, только фиксируются временные метки. Множество баз данных включают временные функции, включая PostrgreSQL, IBM Db2 и Snowflake.
Нет времени лучше настоящего
В то время как вышеупомянутые языки, отладчики и базы данных пытаются манипулировать состояниями во времени (в просторечии “путешествие во времени”), информатика и программирование долгое время стремились смоделировать время в формальной логике, которая может использоваться более детерминированным образом, чем просто временная метка с помощью DateTime. Параллелизм, в частности проверка систем параллелизма с разделяемыми переменными, был давней проблемой программной инженерии. Существует даже ежегодная конференция, посвященная этому.
Формальная логика разработала системы для рассуждений о времени, включая интервально-временную логику (ITL), которая изначально была разработана для определения и проверки конструкции оборудования. Он использует конечные последовательности и предполагает линейное время, поэтому полезен для проверки многопоточной логики в аппаратном обеспечении.
Ряд дополнительных языков программирования использовали различные спецификации временной логики для проверки программной и аппаратной логики. Tokio использовал ITL, в то время как Templog и Chronolog использовали логику линейного времени, а Temporal Prolog основан на линейной и ветвящейся временной логике. Все это выросло из Prolog, языка программирования, разработанного для логических программ.
Работа с этими языками означает преодоление довольно сложной кривой обучения и понимание концепций и обозначений любой системы временной логики, используемой в этих языках.
Таким образом, существует ряд языков / инструментов моделирования, анализа и верификации, которые позволяют моделировать время и состояние, не требуя понимания временной логики:
- TLA+: язык высокого уровня для моделирования программ и систем, особенно распределенных систем, основанный на математике.
- Alloy: программный язык и анализатор для моделирования программ и проверки согласованности проектов программного обеспечения. Он был вдохновлен языком спецификаций Z и реляционным исчислением Тарского, а также находился под влиянием языков моделирования, таких как UML.
- Promela и SPIN: язык моделирования для параллельных систем, который используется с SPIN model checker для проверки свойств этих моделей.
- UPPAAL: Инструмент для моделирования, валидации и верификации систем реального времени путем представления их в виде сетей временных автоматов. Это не столько язык программирования, сколько инструмент визуального моделирования.
- Event-B: формальный метод моделирования и анализа на системном уровне, который использует теорию множеств и математические доказательства для проверки согласованности системы.
- Maude: язык высокого уровня, который использует как уравнения, так и логику перезаписи, которая имеет дело с изменениями состояния в параллельных системах.
Большинство этих языков темпоральной логики и систем моделирования сосредоточены на подборе правильного времени для изменения состояния в многопоточных параллельных системах, работающих полностью в настоящем. В следующем разделе мы рассмотрим некоторые теоретические идеи, которые рассматривают фактические прошлые и настоящие состояния как ресурсы, к которым программа может получить доступ в настоящем.
Будущее изменчиво
Хотя перемещение во времени в настоящее время невозможно, общая теория относительности предполагает, что время может двигаться в обоих направлениях, поэтому физики пытались разобраться с математикой, которая сделала бы это возможным. Были предложены всевозможные дикие вещи, от сверхплотных объектов бесконечной длины, вращающихся со скоростью в четверть скорости света, до зеркал, отражающих волны в обратном направлении во времени.
С помощью этих вычислений и спекуляций физики также перенесли споры о парадоксе дедушки из области ночных дежурств в академические журналы. В книге 1979 года (переведенной на английский в 1983 году) астрофизик-теоретик и космолог Игорь Новиков предположил, что “замкнутые времениподобные кривые” могут допускать перемещение назад во времени до тех пор, пока данные на кривой остаются самосогласованными либо потому, что они уже существовали, либо потому, что состояние прошлого было приведено в соответствие. Это принцип самосогласованности Новикова, который возможно, знают как закон сохранения истории.
Ученый-компьютерщик и футуролог Ханс Моравек увидел это и придумал способ использовать это для быстрого решения сложных проблем. С помощью логики временного цикла Моравек предположил, что, используя схему с отрицательной временной задержкой, вы могли бы вычислить результат, который был бы отправлен обратно в исходное время и состояние. Чтобы не нарушать принцип Новикова, правильный ответ должен появиться сразу. Загвоздка, как будет рассмотрено в последующих статьях, заключается в том, что многие из этих сложных проблем будут сведены к проблеме остановки; то есть определения того, будет ли компьютер когда-либо выключен. Если вы рассчитываете наилучшие результаты и отправляете их назад во времени, вам все равно придется выполнять вычисления в будущем.
Если вам нужны примеры кода с логикой временных циклов, кто-то, используя дескриптор marak, создал их. Эта теоретическая программа доступна через Node.js, благодаря ее способности к параллельной обработке. Это был бы взломщик паролей методом перебора, который, учитывая, что компьютер может работать вечно, мог бы взломать практически любую схему шифрования. Возможность квантовых компьютеров уже заставила исследователей безопасности искать более безопасные алгоритмы; можете ли вы представить себе хаос, вызванный взломом методом перебора во временной петле?
К счастью, любое реальное путешествие во времени все еще находится в области теории. Вы можете поиграть с некоторыми из языков, которые мы описали в этой статье, чтобы использовать некоторые интересные концепции программирования, которые нарушают линейный поток программы или получают четырехмерные представления о состоянии оборудования и программного обеспечения, но вы не можете отправить завтрашние лотерейные номера назад во времени.
Пока.
Смотрите другие наши статьи,подписывайтесь на канал чтобы не пропустить интересное.