Обратное свойство ромба
May. 31st, 2018 02:47 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
codedotЯ тут задумался об обратимых вычислениях. Как они могли бы выглядеть в сетях взаимодействия? Но прежде всего, в каком смысле надо понимать обратимость, если отношение редукции обладает свойством ромба? И что из этого будет следовать?
Пока у меня ничего толком не устоялось, рабочее определение обратимой системы взаимодействия такое: 1) для любой подсети Ν должно быть не более одной активной пары α><β, которая редуцируется к N, и 2) если две подсети M и N - результы взаимодействия активных пар α><β и γ><δ, соответственно, то M и N не пересекаются. Речь идет лишь о подсетях и активных парах, так как об обратимости конфигураций говорить нельзя, когда в сети больше одной активной пары. Не уверен, что это исчерпывающий список условий, но уже их достаточно, чтобы заметить пару-тройку следствий.
Одно из следствий такого определения немедленно накладывает ограничения на правила взаимодействия. В частности, правая часть каждого правила обязана быть связной сетью. Доказательство от противного: строим простой контрпример с двумя одинаковыми активными парами, взаимодействие которых приводит к двум неразличимым сверткам для каждой активной пары, нарушая условие (2). Также потребуется асимметрия правой части правила для α><β, если α и β различны. Продолжу думать в этом направлении позже, хотя уже предчувствую трудности с интерпретацией обратимых систем взаимодействия в исчислении взаимодействия. Например, придется как-то выкручиваться с разыменованием (indirection), применение которого сугубо неоднозначно.
Но самое интересное свойство обратимых систем взаимодействия - это, наверное, обратное свойство ромба. Получается, если такие системы вообще существуют, они одновременно будут обладать и прямым (strong confluence), и обратным (strong upward confluence) свойствами ромба. Это, конечно, мне напомнило об упражнении 3.5.11 (vii) у Барендрегта. Когда я бегло проходил по упражнениям к нескольким главам три года назад, мне не удалось быстро его решить. Было обидно.
Задача была показать, что для термов (λx.b x (b c)) c и (λx.x x) (b c), принадлежащих Плоткину, не существует общей β-экспансии, хотя они оба редуцируются к b c (b c). Эти два терма служат контрпримером для "обратного свойства Черча-Россера" β-редукции. Сегодня я решил поискать, как именно выводить противоречие из существования их общей β-экспансии, и нашел "An Easy Expansion Exercise" (Vincent van Oostrom). Там предлагается использовать теорему о стандартизации. Правда, я не очень понял, как ограничиться материалом конкретно третьей главы.
Update. In a reversible interaction system (RIS), the right-hand side (RHS) of each rule needs to include at least one agent, that is RHS cannot be a wiring: RHS of α[x, x]><β is ambiguous, α[x]><α[x] violates condition (1) in the definition of RIS, and more than one wire make a disconnected net, violating condition (2). As a consequence, in the interaction calculus, each name in an interaction rule needs to have at least one of its two occurrences in a term that is not a name; otherwise we have a disconnected subnet in its RHS. Now it is easy to see strong upward confluence in RIS.
Пока у меня ничего толком не устоялось, рабочее определение обратимой системы взаимодействия такое: 1) для любой подсети Ν должно быть не более одной активной пары α><β, которая редуцируется к N, и 2) если две подсети M и N - результы взаимодействия активных пар α><β и γ><δ, соответственно, то M и N не пересекаются. Речь идет лишь о подсетях и активных парах, так как об обратимости конфигураций говорить нельзя, когда в сети больше одной активной пары. Не уверен, что это исчерпывающий список условий, но уже их достаточно, чтобы заметить пару-тройку следствий.
Одно из следствий такого определения немедленно накладывает ограничения на правила взаимодействия. В частности, правая часть каждого правила обязана быть связной сетью. Доказательство от противного: строим простой контрпример с двумя одинаковыми активными парами, взаимодействие которых приводит к двум неразличимым сверткам для каждой активной пары, нарушая условие (2). Также потребуется асимметрия правой части правила для α><β, если α и β различны. Продолжу думать в этом направлении позже, хотя уже предчувствую трудности с интерпретацией обратимых систем взаимодействия в исчислении взаимодействия. Например, придется как-то выкручиваться с разыменованием (indirection), применение которого сугубо неоднозначно.
Но самое интересное свойство обратимых систем взаимодействия - это, наверное, обратное свойство ромба. Получается, если такие системы вообще существуют, они одновременно будут обладать и прямым (strong confluence), и обратным (strong upward confluence) свойствами ромба. Это, конечно, мне напомнило об упражнении 3.5.11 (vii) у Барендрегта. Когда я бегло проходил по упражнениям к нескольким главам три года назад, мне не удалось быстро его решить. Было обидно.
Задача была показать, что для термов (λx.b x (b c)) c и (λx.x x) (b c), принадлежащих Плоткину, не существует общей β-экспансии, хотя они оба редуцируются к b c (b c). Эти два терма служат контрпримером для "обратного свойства Черча-Россера" β-редукции. Сегодня я решил поискать, как именно выводить противоречие из существования их общей β-экспансии, и нашел "An Easy Expansion Exercise" (Vincent van Oostrom). Там предлагается использовать теорему о стандартизации. Правда, я не очень понял, как ограничиться материалом конкретно третьей главы.
Update. In a reversible interaction system (RIS), the right-hand side (RHS) of each rule needs to include at least one agent, that is RHS cannot be a wiring: RHS of α[x, x]><β is ambiguous, α[x]><α[x] violates condition (1) in the definition of RIS, and more than one wire make a disconnected net, violating condition (2). As a consequence, in the interaction calculus, each name in an interaction rule needs to have at least one of its two occurrences in a term that is not a name; otherwise we have a disconnected subnet in its RHS. Now it is easy to see strong upward confluence in RIS.
