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