MELL Proof Netsに関する細かい話.
代入表現の文脈で,こんな規則が登場することがある1:
Promotion Boxに
(余談だが,少なくとも
多くの文献では,
これらの文献に倣い,
exponentialのセルの役割は,論理式の複製,削除である.つまり,exponentialのセルはハイパーリンクとみなしても何ら問題ない.
これらのセルをハイパーリンクとみなすと,
-
は,生のハイパーリンクがBoxの中にあっても外にあっても本質的には同じであることを表す. -
は,ハイパーリンクを終端させる役割を持つが,このようなゴミはなるべくBoxの外に出しておきたい(外にある状態を正規系とする).
のような気持ちが見えてくる.
Vaux, L.: λ-calcul différentiel et logique classique : interactions calcula- toires. Theses, Université de la Méditerranée - Aix-Marseille II (Jan 2007), https://theses.hal.science/tel-00194149
P. Tranquilli, Intuitionistic differential nets and lambda-calculus, Theoretical Computer Science, vol. 412, no. 20, pp. 1979–1997, (2011) https://doi.org/10.1016/j.tcs.2010.12.022. MELLではなくDifferential Interaction Netsについての話だが...
Di Cosmo, R., Guerrini, S.: Strong Normalization of Proof Nets Modulo Structural Congruences. In: Narendran, P., Rusinowitch, M. (eds.) Rewriting Techniques and Applications. pp. 75–89. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)
Accattoli, B.: Linear Logic and Strong Normalization. In: van Raams- donk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), vol. 21, pp. 39–54. Schloss Dagstuhl – Leibniz-Zentrum für Infor- matik, Dagstuhl, Germany (2013). https://doi.org/10.4230/LIPIcs.RTA.2013.39, iSSN: 1868-8969