Лямбда-исчисление для обратимых (вычислимых по Тьюрингу) функций

19

Мне интересна концепция «полноты р-Тьюринга», определенная Аксельсеном и Глюком (2011) . Система полна r-Turing, если она может вычислять тот же набор функций, что и обратимая машина Тьюринга, без создания каких-либо «мусорных» данных. Это то же самое, что возможность вычислять каждую функцию, которая является (а) вычислимой и (б) инъективной.

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

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

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

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

  • Полный язык r-Turing - вычисляет все вычислимые обратимые функции и может вычислять только обратимые функции
  • Синтаксис и семантика минимально возможны. (Например, лямбда-исчисление имеет только определения функций и приложения, и ничего более.) Нет необходимости связывать синтаксис или семантику с таковыми в лямбда-исчислении, хотя они могут быть.
  • Программа = данные. То есть программы работают с выражениями, а не с данными любого другого типа. Это гарантирует, что вывод программы всегда может быть интерпретирован как программа. Это, вероятно, подразумевает, что это должен быть функциональный, а не императивный стиль языка.
  • Существует какой-то систематический способ преобразования программы в ее обращение, которое не требует существенно большего количества вычислений, чем то, которое требуется для фактического выполнения обратного вычисления. (Не все обратимые языки имеют это свойство, но некоторые имеют.)

Я должен подчеркнуть, что подход Аксельсена и Глюка к обратимым вычислениям весьма отличается от хорошо известного подхода благодаря Беннетту, где (в общем случае необратимая) программа становится обратимой, возвращая некоторую информацию об истории вычислений вместе с выходными данными. Полнота r-Turing - это возможность вычислять инъективные функции без какого-либо дополнительного вывода. Есть несколько вещей, называемых вариациями «обратимого лямбда-исчисления», которые обратимы в смысле Беннета - это не то, что я ищу.

Натаниель
источник
r-Turing complete кажется относительно новым определением, и было бы полезно увидеть доказательство того, что оно не совпадает с полным Turing и интерпретациями / анализами других авторов, отличными от тех, кто ввел концепцию (& не ссылки с оплатой за просмотр, если возможно)
vzn

Ответы:

4

Я не очень знаком с этой областью, но есть некоторые недавние работы сообщества языков программирования, которые могут вас заинтересовать, основанные на идее ограничения языком изоморфизмов типов. В частности, вы могли бы взглянуть на

  • Дробные типы : Рошан П. Джеймс, Захари Спаркс, Жак Каретт и Амр Сабри

а также различные связанные публикации, которые вы можете найти на сайте Амр Сабри .

Ноам Цайлбергер
источник