deep-econom (deep_econom) wrote,
deep-econom
deep_econom

ссылка на память

---
Cedille: Полиморфное лямбда-исчисление с выводимой индукцией
https://akuklev.livejournal.com/1271526.html
Некоторое время назад Aaron Stump сотоварищи предложил интересный вариант полиморфного лямбда-исчисления, где существуют кодировки широчайшего класса индуктивных типов данных, для которых выводима индукция. В этом посте я хотел обрисовать идеи его подхода.

Стартовой точкой подхода Стумпа является наблюдение (сделанное не им, и очень давно), что термы, реализующие рекурсию, и термы реализующие индукцию, после стирания ти́повых аннотаций (англ. erasure), становятся одинаковыми.

Давайте начнём с натуральных чисел и рекурсии. Пусть у нас есть функция f : Nat ⟶ Nat. Как будет выглядеть функция высшего порядка, которая повторяет наше f n раз?
---
Subscribe

  • Трейдинг. Инвестирование, некоторые тезисы по Баффету.

    Конспекты собраний акционеров компании Баффета — Berkshire Hathaway с 1986 по 2015 год. Книга Университет Berkshire Hathaway: 30-летний опыт…

  • Что такое аксиоматика?

    Аксиоматика (набор аксиом). Аксиоматика = система синтаксических уравнений определяющих свойства имён, которые входят в эту систему. Пояснение.…

  • Часы = частотомер.

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

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 0 comments