deniok

А вот, кстати, при проверке лямбда-калькуляторов, написанных студентами, возникла такая задачка.

Пускай мы реализовали на Хаскелле лямбда-термы

data Term = 
    Var String
  | App Term Term
  | Lam String Term        

проверку их альфа-эквивалентности (можно и точное совпадение, для наших целей не важно):

alphaEq :: Term -> Term -> Bool

и одношаговую бета-редукцию (нормальную, для определенности, хотя это тоже не важно):

reduce :: Term -> Term

В последнем случае при отсутствии редексов просто возвращается исходный терм.

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

reduceToNF :: Term -> [Term]
reduceToNF = unfoldr step where 
  step t = 
      let next = reduсe t in 
    if t `alphaEq` next 
    then Nothing 
    else Just (t, next)

Не видите ли вы червоточины в этой схеме?

Сделал в ру-Википедии статью про сабж. Еле поспел к Рождеству.  Держите.

В чистой бестиповой лямбде обычное кодирование булевых значений таково

  tru = λt f. t
  fls = λt f. f

При этом условный оператор кодируется так:

  iif = λb x y. b x y

а основные булевы функции так

  not = λb t f. b f t
  and = λa b. a b fls
  or  = λa b. a tru b

Что из этого получится в просто типизированной системе?

Напомним, что просто типизированная лямбда строится следующим образом. Берём за основу бесконечное множество переменных

  Var = {a,b,c,d,...}

Индуктивно определяем, что тип это либо переменная, либо (правоассоциативная) стрелка между типами

  Type = Var | Type -> Type

Затем задаём правила приписывания типов термам - правила вывода типов. Переменной можно приписать любой тип, абстракции - стрелочный

   x:A    M:B
----------------
(λx. M):(A -> B)

Что касается аппликации, то тип левого аппликанда должен быть стрелочным:

 M:(A -> B)  N:A
-----------------
   (M N): B

Здесь метапеременные M и N обозначают произвольные термы, а метапеременные A и B --- произвольные типы.

Вернёмся к типизации булевых термов и функций. Если приписать булевым термам <<простой>> тип, получим

  tru : a -> b -> a
  tru = λt f. t

  fls : a -> b -> b
  fls = λt f. f

Хотелось бы иметь одинаковый тип для истины и лжи, поэтому естественно приписать t и f один и тот же тип (a). Тогда, введя <<сокращение>>

  Bool = a -> a -> a

можем писать желаемые утверждения типизации

  tru : Bool
  fls : Bool

Однако, к сожалению, всё не так просто. Если посмотреть на условный оператор

  iif : Bool -> s -> s -> s
  iif = λb x y. b x y

то возникает такая проблема. Хотелось бы применять iif к значению любого конкретного типа s, но тогда правила вывода дадут

  Bool  = s -> s -> s

Получается, что наш Bool плохо инкапсулирует свои внутренности. Это приводит к проблемам с типизацией. Например, непонятно, какой тип выведется у b в

  problem = λb. pair (iif b 1 2) (iif b "Ann" "Bob")

Есть два выхода.

Выход (1). Расширение просто типизированной лямбды булевыми константами.

(a) ввести константы true, false и iif в термы, как атомы;
(b) ввести константу Bool в типы, как атом;
(c) ввести дополнительные правила типизации true:Bool, false:Bool и схему правил для любого типа s:

  iif : Bool -> s -> s -> s

(d) ввести схему аксиом δ-редукции: для любых типа s и термов x:s и y:s

  iif true  x y  -δ->  x
  iif false x y  -δ->  y

Выход (2). Расширение просто типизированной лямбды до полиморфной лямбды (System F).

  Bool = forall a. a -> a -> a

При таком подходе в терме

  iif = λb x y. b x y

в теле лямбды перед применением b к x:s происходит (неявное) применение полиморфного значения b : forall a. a -> a -> a к типу s. Эта аппликация терма к типу нужна для того, чтобы <<мономорфизировать>> дотоле полиморфный тип b для дальнейшего использования. Можно эту аппликацию (b s : s -> s -> s) писать явно:

  iif : (forall a. a -> a -> a) -> s -> s -> s
  iif = λb x y. b s x y

UPD. Ну и для полноты картины стоит отметить, что System F должна быть <<оборудована>> ещё и абстракцией терма по типу, которая часто записывается в виде большой лямбды. При этом определение iif принимает окончательный вид

  iif : forall s. (forall a. a -> a -> a) -> s -> s -> s
  iif = Λs. λb x y. b s x y

Всем, кто интересовался курсом, который я читаю в Computer Science клубе при ПОМИ РАН.

Лекториум.тв выложило видео первых 6 лекций (ну точнее пяти с половиной, поскольку на третью лекцию они опоздали:)

Придумал задачку по лямбда исчислению.

Общеизвестен лямбда-терм, не имеющий нормальной формы

(\x.xx)(\x.xx)

Этот терм обладает следующим свойством: он воспроизводит сам себя при каждой бета-редукции, ведя себя по отношению к ней как экспонента по отношению к дифференцированию.

А теперь задача: написать не имеющий нормальной формы терм, который бы вел себя как e^(-x). То есть при первой бета-редукции он должен превращаться во что-то другое, а при следующей возвращаться к исходному виду. Моя версия такого терма (flipflop) под катом белым цветом
( Ответ тут, белым цветом... )
Может кто придумает попроще?

UPD: Эх, а у меня-то решение неправильное :) (Потому что у меня аж шесть шагов) Правильное - у lomeo в комментах.

Для чего нужна Π-абстракция при наличии зависимых типов?

( А вот для чего... )

В 1997 небезызвестные Simon Peyton Jones и Erik Meijer предложили промежуточный внутри-компиляторный богато-типизированный язык Henk. Сегодня я понял причину, почему язык так назван. Механизм - тот же, что и в Хаскелле.

Henk Barendregt - голландский логик,  изобретатель лямбда-куба (1991), автор штудируемого мною нынче Lambda Calculi with Types. "Восхищайтесь" (с)thesz

Нашел ссылку на блестящий пост Lennart Augustsson в его блоге о зависимых типах и не только.

Спасибо asviraspossible.