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

Category:

лямбда-исчисление

Ещё одно введение в теории типов
В математике понятие “теория типов” развивается, и ещё непонятно в какой общности нужно будет давать определение. В контексте информатики теориями типов называют обобщения λ→ — просто типизированного лямбда-исчисления.

В сущности, теория типов — набор правил, которые позволяют конструировать выражения из подвыражений, в ситуации когда не любые выражений комбинируются, а только правильно стыкующиеся. Чтобы выразить “стыкуемость” вводится понятие типов (и набор правил, как эти типы записывать). Если терм x имеет тип T, пишут x : T. В λ→ всегда имеется какой-то набор базовых типов (например, тип Nat, содержащий все натуральные числа), и типы, получаемые из базовых X и Y путём применения оператора X -> Y.

подробнее
Ещё одно введение в теории типов
https://akuklev.livejournal.com/1294373.html
Subscribe

  • (no subject)

    Вирусологи объявили месяц карантина. Сложный выбор для героя: остаться дома или оседлать коня и отправиться исследовать земли половцев и печенегов?…

  • классификация наук

    классификация наук: естественные - физика, химия... неестественные - история, философия... противоестественные - истмат, диамат... сверхъестественные…

  • суббота

    а ты член армии? а хотел бы? Статус Кво: Теперь ты в армии. Status Quo - In the Army Now https://youtu.be/-CRdK7Sf0i0 не хочешь??? а у тебя есть…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 0 comments