deniok: (typed lambda)
Знаете ли вы, чем замечателен этот λ-терм?
λv.(λy.λz.v(yy)(yz))(λx.(λa.λb.a)x(x(xv)v))(λw.ww)
Он нормализуем, его нормальная форма
λv.v(λx.x)(λw.ww)
Более того он нормализуем сильно, то есть независимо от редукционной стратегии. Однако ему нельзя приписать никакого типа, даже в полной версии System F.

Первый такой терм придумали P. Giannini, F. Honsell и S. Ronchi Della Rocca из Миланского университета в 1987 году. А этот я взял из статьи J. B. Wells, Typability and Type Checking in System F Are Equivalent and Undecidable (1998).

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

Пускай мы реализовали на Хаскелле лямбда-термы
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)


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

deniok: (Default)
  Возьмём терм
pre = \m.m pf pz (\t f.t)
pf = \p f.f(p(\t f.f))(\s z.s(p(\t f.f) s z))
pz = \f.f(\s z.z)(\s z.z)
который работает в бестиповой лямбде предесессором для чисел Чёрча:
pre (\s z.s(s(s z))) ->> \s z.s(s z)
pre (\s z.s(s z)) ->> \s z.s z
pre (\s z.s z) ->> \s z.z
pre (\s z.z) ->> \s z.z
(Рассказывают, что идея подобного предесессора пришла в голову Клини, когда он находился под воздействием веселящего газа при удалении четырёх зубов мудрости.)

Предесессор этот типизируем в просто типизированной лямбде страшным и ужасным типом, который слишком бесчеловечен, чтобы приводить его здесь. Желающие могут find'n'replace точечку на стрелочку (->) и отдаться в руки GHCi. Также типизируемы все его аппликации к числам Чёрча, тип их (в отличие от) благообразен и приятен глазу, ибо ожидаем : (a -> a) -> a -> a.

Имея pre, хочется определить вычитание. Это легко делается в бестиповой системе
minus = \k l.l pre k
Работает ли такой подход в просто типизированной лямбде? На первый взгляд да, тип может быть приписан этому терму, желающие на него взглянуть опять-таки отсылаются в GHCi. К несчастью этот minus умеет, оставаясь типизированным, вычитать числа, не большие единицы. Скажем
minus (\s z.s(s(s z))) (\s z.s z) ->> \s z.s(s z)
ещё работает, обладая пристойным типом (a -> a) -> a -> a на всех 27 шагах редукции (счёт вёлся для нормальной стратегии). А вот вычитание из числа 3 числа 2 хоть и даёт 1 при редукциях, но не позволяет типизировать нередуцированный терм.
minus (\s z.s(s(s z))) (\s z.s(s z)) ->> \s z.s z
Кстати говоря, место где типизация волшебным образом возникает, находится почти в самом начале цепочки редукций. Из 43 шагов этого вычитания 40 последним может быть приписан тип (a -> a) -> a -> a, последний нетипизируемый терм
(\s z.s(s z)) pre (\s z.s(s(s z))) 
а следующий в редукционной цепочке
(\z.pre (pre z)) (\s z.s(s(s z))) 
уже согласен приписать себе обычный числовой тип.

Может кто-нибудь, кстати, придумать более простой, чем предесессор Клини, терм, обладающий таким же свойством: (\s z.s(s z)) term не имеет типа, а единожды редуцированный (\z.term (term z)) уже типизируем?

 
deniok: (Default)
Сделал в ру-Википедии статью про сабж. Еле поспел к Рождеству.  Держите.
deniok: (Default)
Митчелл, Основания языков программирования, перевод под ред. Н.Н.Непейводы.

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

5.2.1. Домены (domain). Переведено как области.

8.3.3. Конфлюэнтность (confluence). Переведено как сходимость.

9.4. Экзистенциальные типы (existential types). Переведено как объёмные типы (видимо перепутано с extensional, термин extensionality действительно присутствует, скажем в 8.2.5).

В целом качество перевода кажется мне довольно посредственным. Несколько раз, чтобы понять о чём речь, мне приходилось заглядывать в англоязычный оригинал.
deniok: (typed lambda)
В чистой бестиповой лямбде обычное кодирование булевых значений таково
  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
deniok: (lambda cube)
На Лекториум.тв выложено видео двух последних лекций: про полиморфные системы и их свойства.

http://www.lektorium.tv/course/?id=22797

Лекция 7.
Полиморфные системы в стиле Карри. Сильный и слабый полиморфизм. Типы в контекстах. Введение и удаление $\forall$. Проблемы разрешимости в полиморфном λ-исчислении в стиле Карри. Let-полиморфизм. Полиморфизм высших рангов. Система в стиле Чёрча. Универсальные абстракция и применение. Импредикативность. Связь между λ2 в стиле Карри и Черча. Сильная нормализация. Интерпретации $\forall$-типов. Параметричность.

Лекция 8.
Интуиционистская пропозициональная логика второго порядка. Представление стандартных пропозициональных связок в λ2. Экзистенциальные типы. Пустой тип, булев тип, произведение и сумма типов. Типы для чисел Чёрча и списков. Индуктивные типы.

Слайды в pdf доступны здесь:
http://logic.pdmi.ras.ru/csclub/courses/systemsoftypedlambdacalculi


Последнюю лекцию рассказывал (ближе к концу) в бешеном темпе, чтобы всё успеть. Надо всё-таки останавливаться в желании впихнуть побольше. Буду стараться.

Про остальные 6 вершин лямбда-куба буду рассказывать в мае (уже на Фонтанке, скорее всего).
deniok: (Default)
Всем, кто интересовался курсом, который я читаю в Computer Science клубе при ПОМИ РАН.

Лекториум.тв выложило видео первых 6 лекций (ну точнее пяти с половиной, поскольку на третью лекцию они опоздали:)
deniok: (typed lambda)
Вышел из печати перевод книжки John C. Mitchell, Foundations for Programming Languages, по поводу недоступности которого я сокрушался пару месяцев назад. Заказать книгу можно в интернет-магазине при издательстве: Джон Митчелл. Основания языков программирования.
deniok: (typed lambda)
Придумал задачку по лямбда исчислению.

Общеизвестен лямбда-терм, не имеющий нормальной формы
(\x.xx)(\x.xx)
Этот терм обладает следующим свойством: он воспроизводит сам себя при каждой бета-редукции, ведя себя по отношению к ней как экспонента по отношению к дифференцированию.

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

UPD: Эх, а у меня-то решение неправильное :) (Потому что у меня аж шесть шагов) Правильное - у [livejournal.com profile] lomeo в комментах.
deniok: (typed lambda)
Отталкиваясь от полученной в прошлом посту просьбы, попытаюсь рассказать о Σ-типах.

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

А вот для чего... )
deniok: (умничаю)
Пара задачек по лямбда-исчислению.

(1) Сконструируйте лямбда-терм F, такой что для любого терма M выполнялось бы
FM = MF


(2) Сконструируйте лямбда-терм G, такой что для любых термов M и N выполнялось бы
GMN = NG(NMG)


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

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

Пусть есть лямбда-терм, который может быть редуцирован к другому лямбда-терму с помощью цепочки обычных бета-редукций:

Сохраняется ли при этом тип? То есть верно ли утверждение

(Двойная стрелочка читается "бета-редуцируемо к")

Ответ под катом... )

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 24th, 2017 03:14 am
Powered by Dreamwidth Studios