Ответы пользователя по тегу Лямбда-выражения
  • Язык с нормальным порядком редукции?

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

    ramntry
    @ramntry Автор вопроса
    О! Нашлась такая вещь: LCI Очень неплохо для начала.
    Ответ написан
    Комментировать