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

  • принцип метамодельного перехода

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

  • ощущения суть символы вещей

    ощущения суть символы вещей очень правильная и точная фраза в любопытном месте --- Об этом словечке «элементы», явившемся плодом двенадцатилетнего…

  • сознание это модель, которые моделируют модели

    я у себя писал не раз в том или ином виде, что мышление это моделирование В мышлении нет ничего, кроме процесса обработки моделей.…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 0 comments