arXiv:1806.07275 [cs.LO]

[codedot]

https://arxiv.org/abs/1806.07275

Upward confluence in the interaction calculus

The lambda calculus is not upward confluent, one of counterexamples being known due to Plotkin. This paper explores upward confluence in the interaction calculus. Can an interaction system have this property? We positively answer this question and also provide a necessary and sufficient condition for stronger one-step upward confluence. However, the provided condition is not necessary for upward confluence as we prove that the interaction system of the linear lambda calculus is upward confluent.

Comments

[juan_gandhi]

Wow. Это какой-то очень серьезный результат, мне кажется.

[codedot]

Было бы круче, если бы удалось показать, что найденные достаточные условия еще и необходимы. Интуитивно кажется, что так должно быть, но кто его знает. В любом случае, надо как-то научиться опровергать обратное свойство Черча-Россера.

Update: Выложил новую версию. Оказалось, что найденное условие необходимо и достаточно для (одношагового) обратного свойства ромба, но не является необходимым для обратного (многошагового) Черча-Россера. Последнее удалось показать для системы взаимодействия линейного λ-исчисления.