deniok: (typed lambda)
Обогатил ру-Википедию стать ей про это дело. Ловите. Надо бы ещё, конечно, понаписать про точное определение и всякие свойства, но пока лень.

UPD: Понаписал про формальности.

UPD2: Добавил типизацию по Карри с классическим примером, демонстрирующим, что System F богаче просто-типа-лямбды. И готовящим читателя к рассуждениям про импредикативность и ограниченные версии System F.

UPD3: Уф. Доделал-таки.

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)
Очень хорошие лекционные заметки Femke van Raamsdonk'а из Vrije Universiteit Amsterdam. Курс похож на тот, что я читал в CS Club'е при ПОМИ, но с несколько большим уклоном в логику и примерами с использованием Coq.
Рекомендую своим студентам как полезное дополнительное чтение и удобное введение в Coq.
deniok: (typed lambda)
В импликационном фрагменте классической пропозициональной логики у нас нет никаких связок кроме импликационной стрелочки. Поэтому мы не можем записать закон двойного отрицания или закон исключённого третьего - у нас для этого нет соответствующей связки. Однако имеется закон Пирса ((α → β) → α) → α, который в классической логике полностью эквивалентен упомянутым законам.

В просто типизированной лямбде тип ((α → β) → α) → α необитаем, поскольку соответствие Карри-Говарда задаёт изоморфизм с интуиционистской логикой, которая отличается от классической как раз отсутствием всех этих законов. Однако имеется слабый закон Пирса ((((α → β) → α) → α) → β) → β, про который известно, что он верен интуиционистски, а значит может быть получен конструктивно.

Откуда возникает задача: написать в просто типизированном лямбда-исчислении замкнутый терм типа ((((α → β) → α) → α) → β) → β.

Комменты не скринятся; Coq-читерам предлагается забыть про тактику auto и вспомнить про intros, apply и exact :)
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)
Хорошая задачка из Herman Geuvers, Introduction to Type Theory (упражнение 3.17):

Построить лямбда-терм с типом ((α → β) → α) → (α → α → β) → β.

Ответы скринить не буду.

UPD: Имеется в виду просто типизированная лямбда. То есть fix и прочие Y-комбинаторы нам недоступны.

UPD2: Рекурсия ни в каком виде недоступна!

Profile

deniok: (Default)
deniok

April 2017

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

Syndicate

RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 25th, 2017 02:53 pm
Powered by Dreamwidth Studios