Матчинг дебрёйнизированных термов

[arseniiv]

Вот например у меня есть терм $\forall x\varphi$, где $x,\varphi$ — метапеременные (двух разных сортов). Если позаменять все связанные переменные индексами де Брёйна в терме $\forall x\varphi$ с обычными переменными, получится $\forall\varphi$, что не годится для метапеременных, потому что никак не показано, что в $\varphi$ замкнута переменная $\#0$, а я хочу потом заниматься с ними унификацией и прочими неприличными вещами. Какие к этому подходы, если не хочется отказываться от дебрёйновского представления?

-- Сб фев 17, 2018 01:52:50 --

Ой, я написал что-то не совсем то. Сейчас подумаю о переформулировке.

-- Сб фев 17, 2018 02:09:17 --

А, ну да, вот возьмём небезызвестную аксиому $\forall x\varphi\to \varphi[t/x]$. Её можно разделить на обычную формулу с метапеременными $\forall x\varphi\to \varphi'$ и условие $\varphi' \equiv \varphi[t/x]$. Второе будет использоваться при унификации, а вот в первой надо как-то указать замыкание икса. В голову приходит только подобное же условие $\varphi''\equiv\varphi{\uparrow}[\#0/x]$ (и дебрёйнизованная формула превращается в $\forall\varphi''\to\varphi'$), но можно же, наверно, что-то чуть удобнее придумать и как-то побезопаснее (каждая стрелочка поднятия $\uparrow$ индексов должна быть в паре с квантором или в общем случае с другим каким-то связывателем, как бы это гарантировать попроще?).

-- Сб фев 17, 2018 02:12:59 --

Или, может, наоборот, сделать $\forall\varphi\to \varphi'$ и условие $\varphi'\equiv\varphi{\downarrow}t$, где ${\downarrow}t$ означает $[t/\#0]{\downarrow}$. Но опять же это как-то не очень безопасно, кажется.

[Geen]

arseniiv в сообщении #1292915 писал(а):

а вот в первой надо как-то указать замыкание икса.

Вероятно я что-то существенное не знаю, но, кажется, главное "определить", что он есть в фи...

[arseniiv]

Так поначалу ничего там нет, это просто переменная. Вот когда мы будем унифицировать посылки и результат какого-нибудь правила вывода с реальными формулами из вывода, там будет что-то, условно говоря, подставляться.

-- Сб фев 17, 2018 02:50:50 --

Я тут просто решил свелосипедить систему почти такую же общую как Metamath, но манипулирующую не строками, а нормальными такими деревьями разбора, заодно использовать пользу от индексов де Брёйна вместо связанных переменных и не синтаксическую подстановку (тем более в полной общности я не могу её выразить — в Metamath она выражается средствами языка первого порядка).

[_Ivana]

Я конечно не лингвист и не понимаю настолько глубоко озвученную проблему, но на кустарном уровне могу предположить следующий вариант - терм кодируется дебрейном связанные переменные и буквами/символами свободные. Свободные могут болтаться "просто так" - и тогда мы при матчинге сравниваем их буквально, как элементы алфавита (цифры дебрейновские сравниваются тривиально), а могут быть заданы в некоем контексте существования терма - тогда мы берем их значения из контекста (возможно рекурсивно до упора в полного дебрейна - если они просто синонимы других комбинаторов, например вместо каждоразового расписывания одних и тех же известных функций, в термах просто задаются их символьные синонимы в контексте). Но тогда задача матчинга двух термов сводится либо к полной подстановке и раскрытию всех свободных переменных (в общем случае у каждого терма в своем контексте) - и мы избавляемся от них полностью в каждом терме и можем матчить дебрейновкие числа.

Или я не вижу самой сути проблемы - тогда может простой пример поможет прояснить ее?

[arseniiv]

Я сегодня откопал шикарную книгу A. S. Troelstra, H. Schwichtenberg Basic proof theory (совсем по другому поводу, из-за минимальной логики) и получил сразу несколько новых мыслей на счёт этой темы. Ещё немного почитаю то и сё и потом напишу их здесь.

[arseniiv]

_Ivana в сообщении #1293025 писал(а):

Или я не вижу самой сути проблемы - тогда может простой пример поможет прояснить ее?

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

Итак, полезности, которые я почерпнул и надумал. Во-первых, я как-то раньше не задумывался о подтермах, понимаемых не структурно, а более семантически (в книге такие подформулы названы генценовскими), а с дебрёйновскими термами это кстати: непосредственным подтермом некоторого произвольного терма $c(\vec v_1.t_1,\ldots,\vec v_n.t_n)$, где в $t_i$ связаны переменные $\vec v_i$, будут считаться любые термы вида $t_i[\vec t'/\vec v_i]$, в которых никаких внезапных свободных переменных с необходимостью, в отличие от структурных подтермов $t_i$, не возникает.

Во-вторых, можно вообще отщепить отдельно «термы» вида $\vec v.t$, уже к которым применяются конструкторы (фактически это получится вложенное в систему наивное λ-исчисление, ограниченное в правах — со всеми переменными, по которым что-то замкнуто, должно быть что-то сделано, чтобы не было, вольно ассоциируя с физикой, голых сингулярностей — или связать чем-то реальным типа квантора или $\lambda$ предметного языка, или подставить терм). Это я себе на заметку возьму, но неизвестно, решусь ли. Аксиома выше перепишется как $\forall\varphi\to\varphi[t]$ (где сорт $\varphi$ подразумевается $T\to T$, если сорт нормальных термов есть $T$) без всяких сдвигов контекстов и упоминания $\#0$, что хорошо и даёт надежду меньшего числа ошибок в коде, который бы работал с такими усложнёнными термами. Кроме того, вот уже с таким дополнением инкорпорировать «безымянные подстановки» (не чета тем, что выше) в язык тоже можно, завершив вписание λ-исчисления. В итоге для описания, например, правил вывода классической логики может понадобиться только одна вещь, которую запихивать в термы уже нет смысла — ограничения на свободные переменные (что куда-то какие-то не должны входить). Например, правило Бернайса для $\exists$ записать как

$$\dfrac{\varphi[x]\to\psi,\quad\psi\setminus x}{\exists\varphi\to\psi}.$$

Только тут проблема, что в $\exists\varphi$ могуть остаться некоторые свободные вхождения $x$ из тех, которые есть в $\varphi[x]$, т. к. они могут содержаться и в $\varphi[x']$ для $x'\not\equiv x$. Не помню, это проблема по сравнению с классическим изложением или, наоборот, именно в поведении, имеющемся там, меньше смысла — во всяком случае, $\varphi[x]$ всегда будет генценовским подтермом $\exists\varphi$.

Что-то ещё было на уме, но забыл.

[george66]

При деБрёйновской записи подстановка пишется так $\varphi[t/]$
Подставлять будет вместо индекса $0$
Бета-редукция выглядит так
$(\lambda M)N\to M[N/]$
Вычисляя подстановку, мы её двигаем вглубь терма, например
$(M_1M_2)[N/]\to(M_1[N/])(M_2[N/])$
Но не так просто её двигать сквозь лямбду
$(\lambda M)[N/]\to\lambda(M[\Uparrow\!(N/)])$
И ещё нужно штук 10 правил вычисления. Вся теория подстановки (и альфа-конверсии) адски сложная, что ещё усугубляется идиотскими обозначениями. Подстановку, на самом деле, надо писать спереди (точнее, там же, где пишем кванторы и лямбды), тогда надо гораздо меньше скобок. Например, вместо
$(\forall x\varphi)[t/y]$ и $\forall x(\varphi[t/y])$
следует писать
$[t/y]\forall x\varphi$ и $\forall x[t/y]\varphi$
Если хотите в этом разбираться, начните с классической статьи Abadi, Cardelli, Curien, Levy "Explicit substitutions"

[arseniiv]

Да я уже реализовал один раз когда-то давно λ-исчисление с дебрёйновскими термами, всё вплоть до β-редукции (или βη, не помню). Конечно, синтаксически я там подстановку не рассматривал, а сразу делал, раз теория с конкретными (не мета-) переменными была, так что прям уж сложности.

george66 в сообщении #1293165 писал(а):

(и альфа-конверсии)

Кстати, а зачем нам альфа-конверсия в безымянном представлении? Оно ведь как раз от неё избавляет.

george66 в сообщении #1293165 писал(а):

Подстановку, на самом деле, надо писать спереди (точнее, там же, где пишем кванторы и лямбды), тогда надо гораздо меньше скобок.

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

Как мне кажется, теория синтаксических подстановок не нужна для успешной реализации унификации (я до сих пор не начал, а три дня уже прошло, беда) — вот есть у нас ограничения $v_2 = v_1[t'_1/v'_1]$, $v_3 = v_2[t'_2/v'_2]$, так сначала унифицируем $v_1$ и $v_2$, а потом $v_2$ и $v_3$, без надобности получать ограничение вида $v_3 = v_1[\ldots]$.

А вот классическая статья в библиотеке не помешает, спасибо.

∗ ∗ ∗ ∗ ∗

Я вчера напредлагал (если кому-то интересно это читать) лишнего, аппликация и переменные «сложных» сортов не понадобятся, понадобится только парсить $v^{S'}.t^S$ как $(t\uparrow[v/])^{S'\to S}$ (спасибо за обозначение подстановки вместо $\#0$), притом это будет неделимая конструкция, подстановку и сдвиг в виде примитивных операций вводить не понадобится. Чтение подстановки $t[v/t']$ будет давать терм и ограничение, как я и решил изначально, итого на входе будут самые обычные термы с переменными, которые никак не надо модифицировать; всё стало прозрачным и довольно простым, останется только проверить в работе.

[arseniiv]

А вот нет, прозрачным-то прозрачным, но бестолковым. Если сделать в точности так, как предложил, не выйдет в итоге получить пользу от индексов. С другой стороны, а чего я хотел, с метапеременными-то — в таком случае упростить можно только $x[t/x] \mapsto x$, а любая другая метапеременная может содержать что угодно, если не добавлено ограничений (например типа как в Metamath, если $y$ и $x$ не должны заменяться термами, содержащими одну и ту же переменную, то тогда можно $y[t/x] \mapsto y$). Хотя не факт, что распространение подстановок по подтермам или отказ от индексов чем-то тут может помочь.