Мне интересна концепция «полноты р-Тьюринга», определенная Аксельсеном и Глюком (2011) . Система полна r-Turing, если она может вычислять тот же набор функций, что и обратимая машина Тьюринга, без создания каких-либо «мусорных» данных. Это то же самое, что возможность вычислять каждую функцию, которая является (а) вычислимой и (б) инъективной.
Я хотел бы вычислительно исследовать пространство вычислимых инъективных функций. Для этого я ищу «самый минимальный» обратимый язык программирования - то, что может играть эквивалентную роль для вычислимости r-Тьюринга, которую лямбда-исчисление играет для вычислимости Тьюринга.
Я знаю, что есть много обратимых языков, которые люди разработали и доказали свою полноту. Однако они разрабатываются с учетом практического применения, и поэтому их авторы концентрируются на том, чтобы придать им выразительные функции, а не сделать их минимальными.
Кто-нибудь знает, был ли описан такой минимальный обратимый язык, или есть какие-либо исследования в этом направлении? Я довольно новичок в литературе по этой теме, поэтому я мог легко пропустить это. Кроме того, есть ли у кого-нибудь понимание того, как такой язык может быть создан?
Ниже приводится краткое изложение того, что я ищу. Я не знаю, может ли он быть создан путем изменения самого лямбда-исчисления, или нужно было бы использовать совершенно другой тип языка.
- Полный язык r-Turing - вычисляет все вычислимые обратимые функции и может вычислять только обратимые функции
- Синтаксис и семантика минимально возможны. (Например, лямбда-исчисление имеет только определения функций и приложения, и ничего более.) Нет необходимости связывать синтаксис или семантику с таковыми в лямбда-исчислении, хотя они могут быть.
- Программа = данные. То есть программы работают с выражениями, а не с данными любого другого типа. Это гарантирует, что вывод программы всегда может быть интерпретирован как программа. Это, вероятно, подразумевает, что это должен быть функциональный, а не императивный стиль языка.
- Существует какой-то систематический способ преобразования программы в ее обращение, которое не требует существенно большего количества вычислений, чем то, которое требуется для фактического выполнения обратного вычисления. (Не все обратимые языки имеют это свойство, но некоторые имеют.)
Я должен подчеркнуть, что подход Аксельсена и Глюка к обратимым вычислениям весьма отличается от хорошо известного подхода благодаря Беннетту, где (в общем случае необратимая) программа становится обратимой, возвращая некоторую информацию об истории вычислений вместе с выходными данными. Полнота r-Turing - это возможность вычислять инъективные функции без какого-либо дополнительного вывода. Есть несколько вещей, называемых вариациями «обратимого лямбда-исчисления», которые обратимы в смысле Беннета - это не то, что я ищу.
источник
Ответы:
Я не очень знаком с этой областью, но есть некоторые недавние работы сообщества языков программирования, которые могут вас заинтересовать, основанные на идее ограничения языком изоморфизмов типов. В частности, вы могли бы взглянуть на
а также различные связанные публикации, которые вы можете найти на сайте Амр Сабри .
источник