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
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 0 comments