типизация λ-исчисления (Барендрегт)

[Mysterious Light]

читаю статью Барендрегта 'Introduction to generalized type systems'.

Цитата:

Ones there are types depending on terms one may introduce cartesian products. Suppose that for each $a:A$ a type $B_a$ is given, and that there is an element $b_a:B_a$. Then we may want to form the function $\lambda a:A.b_a$ that should have as type the cartesian product $\Pi a:A.B_a$ of the $B_a$s. Ones there product types are allowed, the function space type of $A$ and $B$ can be written as $(A\rightarrow B)=\Pi a:A.B\;(=B^A, \mathrm{informally})$.

Не могу понять этот абзац, а без него не получается понять "глубокий смысл".
Объясните, пожалуйста, что означает П и, в частности, почему последнее выражение с ним является экспоненциалом из А в B.

[Xaositect]

$\prod$ - это, как там написано, декартово произведение.
Т.е., для каждого $a$ есть тип $B_a$, тогда можно рассмотреть функции $a: A \mapsto b_a: B_a$ как элементы декартового произведения $\left(b_{a_1}, b_{a_2},\dots\right)\in \prod\limits_{a:A} B_a$.

[Mysterious Light]

Ага!, но всё же какое-то непонятное произведение, особенно при $|A|\geq\aleph_0$. Но смысл я понял. Получается, $\Pi$ есть своеобразная форма абстракции, а именно: если $\lambda$ порождает терм во время абстракции, то $\Pi$ порождает его тип. Но если я правильно понял, выражение $\Pi x\colon A.B$ нельзя заменить на $(A\rightarrow B)$, если в $B$ терм $x$ входит явно.

Кроме того, у меня никак не получается разобраться, как "читать" термы (в частности, с П-абстракцией). Например, там же было утверждение для $\lambda 2$:
$\vdash(\lambda\beta\colon *. \lambda a\colon (\Pi\alpha\colon *.\alpha).\: a((\Pi\alpha\colon *.\alpha)\to\beta)a)\; : \; (\Pi\beta\colon *.(\Pi\alpha\colon *.\alpha) \to \beta)$
Если я правильно понял схемы Пи и лямбды, то это есть следствие из
$\beta\colon * \vdash (\lambda a\colon (\Pi\alpha\colon *.\alpha). \; a((\Pi\alpha\colon *.\alpha)\to\beta)a) \; : \; ((\Pi\alpha\colon *.\alpha) \to \beta)$
$\beta\colon *, a\colon (\Pi\alpha\colon *.\alpha)\colon\square \vdash a((\Pi\alpha\colon *.\alpha)\to\beta)a \colon \beta$
Дальше разобрать выражение не получается. В бестиповом исчислении разбор можно было произвести от самых глубоких термов, там очевиден был путь, то же самое касается $\underrightarrow\lambda$. В обоих случаях можно было провести в естественном порядке построение. Тут же у меня возникают сложности за счет одновременной взаимной манипуляции с термами и их типами, а "обратный" разбор (который я попытался проделать выше) останавливается на этом месте.
(К слову, пояснение в статье не помогло, выражение $\vdash (\lambda\beta\colon *.\: \lambda a\colon \bot.\: a\beta) \; : \; (\Pi\beta\colon *.\: \bot\to\beta)$ следует из $\beta\colon *, a\colon \bot \vdash a\beta : \beta (\equiv \bot \left[\alpha\diagup\beta\right])$)

Спасибо за помощь.

[Xaositect]

Mysterious Light в сообщении #483983 писал(а):

Но если я правильно понял, выражение $\Pi x\colon A.B$ нельзя заменить на $(A\rightarrow B)$, если в $B$ терм $x$ входит явно.

Да, зависимые типы "сильнее" функций.

Цитата:

Кроме того, у меня никак не получается разобраться, как "читать" термы (в частности, с П-абстракцией).

Надо просто не забывать, что типы-произведения - это обобщение типов-функций, в частности, их можно применять к элементам, или, в $\lambda2$ - к типам.

Давайте размотаем приведенный пример "изнутри":
$a:(\Pi \alpha : \star. \alpha), \sigma:\star \vdash a\sigma : \sigma$. Т.е. $\bot \equiv \Pi \alpha:\star.\alpha$ - это тип "операторов выбора", которые из каждого типа получают некоторый его элемент .
Отсюда $a:(\Pi \alpha:\star.\alpha),\beta:\star\vdash a((\Pi\alpha:\star.\alpha)\to \beta):((\Pi\alpha:\star.\alpha)\to \beta)$
Далее, применяем полученную функцию $\bot \to \beta$ к $a:\bot$:
$a:(\Pi \alpha:\star.\alpha),\beta:\star\vdash (a((\Pi\alpha:\star.\alpha)\to \beta)a):\beta$
Проводим $\lambda$-абстракцию по $a$:
$\beta:\star\vdash \lambda a :(\Pi \alpha:\star.\alpha). (a((\Pi\alpha:\star.\alpha)\to \beta)a):((\Pi\alpha:\star.\alpha)\to \beta)$
И $\Lambda$-абстракцию по $\beta$:
$\vdash \lambda \beta:\star.\lambda a :(\Pi \alpha:\star.\alpha). (a((\Pi\alpha:\star.\alpha)\to \beta)a):(\Pi\beta:\star.((\Pi\alpha:\star.\alpha)\to \beta))$

[Mysterious Light]

Я очень благодарен Вам за это пояснение!

Подскажите, пожалуйста, литературу, по которой можно будет освоить $\lambda 2$ абстракцию на интуитивном уровне, чтоб смог легко (на уровне очивидного и естественного) манипулировать с термами.

И ещё, если не сложно, проверьте рассуждения (это из упражнений в середине статьи):
$\neg \equiv \lambda \alpha : *.\: \alpha\to\bot$
$\alpha:*,\;x:\neg\alpha,\;y:\alpha \;\vdash xy:\bot$
Значит, $x$ есть однопараметрический (параметр $y$ имеет тип $\alpha$) оператор выбора.
Необходимо сконструировать терм $M$, что $\alpha:*,\beta:*\vdash M:(\alpha\to\beta)\to(\neg\beta\to\neg\alpha):*$
Судя по всему, если имеется $\alpha:*,\beta:*,f:(\alpha\to\beta),y:\beta\to\bot \vdash z:\alpha\to\bot$
то терм $M=\lambda f:(\alpha\to\beta). \lambda y:(\beta\to\bot) . z$ удовлетворяет условию.
Например, терм $z=\lambda x:\alpha.\: y(fx)$ подходит. Значит, $M=\lambda f:(\alpha\to\beta). \lambda y:\beta\to\bot . \lambda x:\alpha.\: y(fx)$ будет ответом.

(Оффтоп)

Вспомнился Haskell, где $(\neg,M)$ был бы назван кофунктором.

[Xaositect]

Есть "Introduction to Type Theory" (http://www.cs.ru.nl/~herman/PUBS/IntroTT.pdf , слайды http://www.cs.ru.nl/~herman/Uruguay2008 ... chool.html)

Mysterious Light в сообщении #484533 писал(а):

И ещё, если не сложно, проверьте рассуждения (это из упражнений в середине статьи):

Верно. Вы, кстати, про изоморфизм Карри-Говарда уже читали?

[Mysterious Light]

Спасибо за ссылки

Про изоморфизм не читал, но слышал (то есть читал, но не вдаваясь в детали, знаю только идею). К чему Вы его вспомнили?

И ещё: можете привести какой-нибудь пример "оператора выбора"? Я пока не представляю, как он должен выглядеть. То есть будет ли хоть один конструктивно построенный терм, который имеет этот тип?

[Xaositect]

Mysterious Light в сообщении #484977 писал(а):

К чему Вы его вспомнили?

Ну, просто $(\alpha\to\beta)\to(\neg\beta\to\neg\alpha)$ - это логический закон контрапозиции, упражнение явно придумано на его основе.
(upd. исправил формулу)

Mysterious Light в сообщении #484977 писал(а):

И ещё: можете привести какой-нибудь пример "оператора выбора"? Я пока не представляю, как он должен выглядеть. То есть будет ли хоть один конструктивно построенный терм, который имеет этот тип?

Нет, $\bot$ не имеет замкнутых обитателей.

[Mysterious Light]

Xaositect в сообщении #485066 писал(а):

Ну, просто $(\alpha\to\beta)\to(\neg\alpha\to\neg\beta)$ - это логический закон контрапозиции

Тогда, по аналогии, $\bot$ означает ложь. Поэтому и нет замкнутых обитателей.

[Mysterious Light]

Прочитал Introduction to Type Theory, сейчас перечитываю её в очередной раз и читаю Lambda calculi with types Барендрегта. Как я и предполагал, начал с тяжелой книги; зато теперь располагаю литературой.
В статье Introduction to Type Theory особо понравился момент, когда устанавливался изоморфизм в случае полиморфизма, и именно:

Цитата:

$\begin{array}{rl} \bot &= \forall \alpha. \alpha \\ \sigma\wedge\tau &= \forall \alpha. (\sigma\rightarrow\tau\rightarrow\alpha)\rightarrow\alpha \\ \sigma \vee \tau &= \forall \alpha. (\sigma\rightarrow\alpha)\rightarrow(\tau\rightarrow\alpha)\rightarrow\alpha \\ \exist\alpha.\sigma &= \forall \beta. (\forall \alpha. \sigma\rightarrow\beta) \rightarrow \beta \end{array}$

Хотя мне всё равно не понятно, почему $\not\vdash_{\lambda 2} x:\forall\alpha.\alpha$ (если доказывать без изоморфизма К.-Х.)
Когда я читал intro to generalized type system, я не мог понять, почему те схемы, общие, описанные там, выражали все частные случаи (λ2 и λ→). Так, например, долго пытался понять, почему в λ→ $\Pi x:A.B \equiv A \to B$, ведь символ $\Pi$ в λ→ не используется. На самом деле, если мы ограничиваемся только (*,*), то нельзя построить тип, зависящий от терма явно.

Сейчас я хочу уяснить для себя схему построения типов данныв в λ. В статье приводятся примеры для типов натуральных чисел и списков. Хочу разобраться с ними и с тем, как можно построить λ-аналог произвольного типа данных.
Рассмотрим, например, тип данных пара. В "Синтаксис и семантика" подробно объясняется, почему $\lambda xyz.zxy$ выражает пару $(x,y)$. Типизируем её:
$\begin{array}{rl} x:A:*,y:B:*, C:* &\vdash_{\lambda_\rightarrow} (\lambda f: A \to B \to C. fxy) : (A \to B \to C) \to C \\ x:A:*,y:B:* &\vdash_{\lambda2} (\lambda f: A \to B \to C. fxy) : \forall C. (A \to B \to C) \to C \\ x:A:*,y:B:* &\vdash_{\lambda2} (\lambda C:*.\:\lambda f: A \to B \to C. fxy) : (\Pi C:*. (A \to B \to C) \to C) \\ & \vdash \mathcal{P} : \mathbb{P} \end{array} \\ \mathcal{P} \stackrel{\textrm{def}}{=} \lambda A:*. \lambda B:*. \lambda x:A. \lambda y:B. \lambda C:*. \lambda f: A \to B \to C. fxy \\ \mathbb{P} \stackrel{\textrm{def}}{=} \Pi A:*.\Pi B:*. A \to B \to (\Pi C:*.(A \to B \to C) \to C) $

Терм $\mathcal{P} : \mathbb{P}$ и есть конструктор пары, $\mathcal{P}AB : \mathbb{P}AB$ есть конструктор пары определенного типа (A,B), а $\mathcal{P}ABxy : \mathbb{P}ABxy \equiv (\Pi C:*. (A \to B \to C) \to C)$ есть конкретная пара (x,y), где x:A и y:B.
Тут я хочу отвлечься от основной мысли. $\mathbb{P}ABxy \equiv (\Pi C:*. (A \to B \to C) \to C)$ при любых x:A и y:B, поскольку мы договорились, что $X \to Y$ обозначается вместо $\Pi z:X.Y$, если z не входит в Y явно. То есть тут механизм отдаленно напоминает K-комбинатор, когда есть определенный результат, совершенно не зависящий от аргумента. В нашем случае, от x и y совершенно не зависит $(\Pi C:*. (A \to B \to C) \to C)$. Как мне лучше записать и аргументировать свою нотацию, если я хочу подчеркнуть связь с $\mathbb{P}AB$? Если б был оператор выбора, можно было б им воспользоваться. А так ведь даже не понятно, не вырождены ли сами A и B.

(Оффтоп)

А ведь тип пары есть, по факту, типом, соотв. по К.-Х. конъюнкции, определение которой я процитировал в начале

Каноническая проекция на первый тип:
Типизирую то, что написано в Семантике и Синтаксисе, а именно: если $p=\lambda xyz.zxy, \mathrm{fst'}=\lambda xy.x\equiv K$, то $p xy\;\mathrm{fst'}=x$ и $\mathrm{fst} = \lambda p. p\;\mathrm{fst'}$ является проекцией.
$A:*,B:* \vdash \mathrm{fst'} \equiv (\lambda x:A.\lambda y:B. x) : (A \to B \to A)$, при фиксированных типах (A,B). Попробую в λ2 сделать абстракцию по типам:
\mathrm{fst} \equiv \lambda A.\lambda B. \lambda p: (\Pi C:*. (A \to B \to C) \to C). p \: \mathrm{fst'} : \\ : \Pi A:*. \Pi B:*. \Pi p: (\Pi C:*. (A \to B \to C) \to C). \; A$
Как я писал выше, хотелось бы подчеркнуть, что $A,B:* \vdash p : \mathbb{P} A B \_ \_$, тогда $\mathrm{fst} : \Pi A. \Pi B. \mathbb{P} A B \_ \_ \to A$

Скажите, пожалуйста, я правильно обобщил тип пары и её проекции?

P.S. не получилось у меня воспользоваться \begin{multline*}\end{multline*}. Пишет Syntax Error.

[Xaositect]

Да, все верно.