Lean: introduction

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

О кодировании натуральных чисел (часть 1)

Широко известно классическое индуктивное объявление натуральных чисел: ноль — натуральное число, и число следующее за натуральным — натуральное. Простейший способ кодирования таких чисел при помощи лямбда-исчисления — метод Чёрча, не имеющий, как кажется, прямого отношения к индуктивному типу.…

Untyped Lambda Calculus

Попытка cделать описание лямбда-исчисления сразу с реализацией кода на языке программирования Haskell.…