2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Матчинг дебрёйнизированных термов
Сообщение16.02.2018, 23:47 
Заслуженный участник
Аватара пользователя


27/04/09
25073
Уфа
Вот например у меня есть терм $\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}$. Но опять же это как-то не очень безопасно, кажется.

 Профиль  
                  
 
 Re: Матчинг дебрёйнизированных термов
Сообщение17.02.2018, 00:18 
Заслуженный участник
Аватара пользователя


01/09/13
2371
arseniiv в сообщении #1292915 писал(а):
а вот в первой надо как-то указать замыкание икса.

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

 Профиль  
                  
 
 Re: Матчинг дебрёйнизированных термов
Сообщение17.02.2018, 00:47 
Заслуженный участник
Аватара пользователя


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

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

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

 Профиль  
                  
 
 Re: Матчинг дебрёйнизированных термов
Сообщение18.02.2018, 05:34 


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

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

 Профиль  
                  
 
 Re: Матчинг дебрёйнизированных термов
Сообщение18.02.2018, 08:56 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: Матчинг дебрёйнизированных термов
Сообщение18.02.2018, 11:11 
Заслуженный участник
Аватара пользователя


27/04/09
25073
Уфа
_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$.

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

 Профиль  
                  
 
 Re: Матчинг дебрёйнизированных термов
Сообщение19.02.2018, 03:15 
Заслуженный участник


31/12/15
650
При деБрёйновской записи подстановка пишется так $\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"

 Профиль  
                  
 
 Re: Матчинг дебрёйнизированных термов
Сообщение19.02.2018, 19:05 
Заслуженный участник
Аватара пользователя


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

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']$ будет давать терм и ограничение, как я и решил изначально, итого на входе будут самые обычные термы с переменными, которые никак не надо модифицировать; всё стало прозрачным и довольно простым, останется только проверить в работе.

 Профиль  
                  
 
 Re: Матчинг дебрёйнизированных термов
Сообщение19.02.2018, 22:01 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 9 ] 

Модераторы: Toucan, maxal, PAV, Karan, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group