Язык с нормальным порядком редукции?

Question

[ramntry]

Необходим язык с нормальным порядком редукции. Такой, чтобы в нем можно было корректно вычислять выражения типа
(λx.y)((λx.xxx)(λx.xxx))

и проверять работоспособность более полезных конструкций, например, рекурсивных лямбда-термов, определенных с помощью Y-комбинатора. Таковые, как известно, способны на очень многое, от простых рекурсивных расчетов факториала до реализации алгоритмов типа foldr, map, filter etc с последующим использованием их для создания еще более сложных конструкций. Порядок редукции и в Lisp, и в Scheme аппликативный, что делает их непригоднымы. Так называемый lazy-диалект Scheme в DrRacket также успешно зацикливается на приведенном выше примере. Возможно, спасение существует в Haskell, тот таки должен для выражения вроде терма в правой части примера лишь создать thunk и благополучно его не вычислять, редуцируя целое выражение, но Haskell имеет строгую и сложную систему типов — он построен на идеях типизированного лямбда-исчисления. А, как известно, тип уже ω-комбинатора λx.xx невычислим. О чем Haskell и заявляет, указывая, что не способен вычислить бесконечно-рекурсивный тип. Вероятно, это возможно победить с использованием расширений типовой системы, как стандартной, так и Glasgo, (существует поддержка т.н. GADT, ключевых слов forall и exists (ага, это именно кванторы)), но очень не хочется убивать приличный объем времени на изучение этих вещей, как и на столь сложную реализацию столь простых идей. Может быть, кто то владеет этими расширениями в Haskell? Или знает подходящий язык? Он может быть сколь угодно игрушечным, всего лишь нужен нормальный порядок редукции. Заранее спасибо.

Answer 1

[ramntry]

О! Нашлась такая вещь: LCI Очень неплохо для начала.

Answer 2

[ramntry]

Выяснилась некоторая деталь: в первую очередь в искомом языке интересна работоспособность Y-комбинатора, поскольку он позволяет решать рекурсивные уравнения, что, в свою очередь, позволяет создавать рекурсивные функции. Однако, не смотря на формальное равенство (конвертируемость) ∀ X ( λ ⊢ Y X =_β X (Y X) ), ни Y X не β-редуцируем к X (Y X), ни наоборот. Существует, однако, лучший в этом смысле и аналогичным по своим практическим возможностям Θ-комбинатор, придуманый Аланом Тьюрингом, а также множество других комбинаторов фиксированной точки (по ссылке также можно найти множество примеров реализации комбинаторов на различных языках, что крайне ценно). Их вычислимость, тем не менее, по-прежнему чувствительна к порядку редукции, но требование нормального порядка избыточно. Существуют помимо понятия нормальной формы терма, понятия головной (или заголовочной) нормальной формы, слабой головной нормальной формы, которые используются в некоторых языках даже с принципиально аппликативным порядком редукции и приводят к тому, что терм-аргумент, едва став λ-абстракцией (в слабом случае), перестает вычисляться и передается в тело функции (сокращается крайний левый внешний редекс, как при нормальном порядке). Это делает возможными в таких языках специальные трюки, которые за счет некоторой модификации канонических комбинаторов (навешивания на них «лишних» λ-абстракторов) добиться нужного порядка вычисления.

Answer 3

[Данияр Супиев]

Насколько я помню, Скала удовлетворяет всем вашим требованиям. Да, типизация там статическая, но именно она и позволяет задать тип бесконечной рекурсии, и вполне нормально с этим живёт. Советую курс progfun на coursera.