# zbMATH — the first resource for mathematics

SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi. (English) Zbl 1184.68469
Summary: We present the system SUBSEXPL used for simulating and comparing explicit substitutions calculi. The system allows the manipulation of expressions of the $$\lambda$$-calculus and of three different styles of explicit substitutions: the $$\lambda\sigma$$, the $$\lambda s_e$$ and the suspension calculus. A variation of the suspension calculus, which allows for combination of steps of $$\beta$$-contraction is included too. Implementations of the $$\eta$$-reduction are provided for each style. Other explicit substitutions calculi can be easily incorporated into the system due to its modular structure. The uses of the system include: the visualization of the contractions of the $$\lambda$$-calculus in de Bruijn notation, and of guided one-step reductions as well as normalization via each of the associated substitution calculi. Many useful facilities are included: reductions can be easily recorded as text files, LaTeX outputs can be generated and several examples for dealing with arithmetic operations and computational operators such as conditionals and repetitions in the $$\lambda$$-calculus are available.
The system can be executed over Emacs using the $$x$$-symbol mode in such a way that $$\lambda$$-terms and terms of the explicit substitutions calculi are represented in its natural syntax avoiding the necessity of repeatedly generating LaTeX outputs. The system has been of great help for systematically comparing explicit substitutions calculi, as well as for understanding properties of explicit substitutions such as the Preservation of Strong Normalization. In addition, it has been used for teaching basic properties of the $$\lambda$$-calculus such as: computational adequacy, the usefulness of de Bruijn’s notation and of making explicit substitutions in real implementations.

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B40 Combinatory logic and lambda calculus
##### Software:
Automath; SUBSEXPL
Full Text:
##### References:
 [1] ABADI M., J. of Func. Programming 1 (4) pp 375– (1991) · Zbl 0941.68542 · doi:10.1017/S0956796800000186 [2] AYALA-RINCON M., The Logical Journal of the IGPL 9 (4) pp 489– (2001) · Zbl 0987.03012 · doi:10.1093/jigpal/9.4.489 [3] AYALA-RINCON M., Annals of Pure and Applied Logic 134 (1) pp 5– (2005) · Zbl 1067.03042 · doi:10.1016/j.apal.2004.06.009 [4] DOI: 10.1017/CBO9781139172752 · Zbl 0948.68098 · doi:10.1017/CBO9781139172752 [5] BARENDREGT H. P., The Lambda Calculus : Its Syntax and Semantics (revised edition) (1984) · Zbl 0551.03007 [6] BRIAUD D., Typed lambda calculi and applications, vol. 902 of LNCS pp 94– (1995) · doi:10.1007/BFb0014047 [7] DE BRUIJN N., Indag. Mat. 34 (5) pp 381– (1972) · doi:10.1016/1385-7258(72)90034-0 [8] DOWEK G., Information and Computation 157 (1) pp 183– (2000) · Zbl 1005.03016 · doi:10.1006/inco.1999.2837 [9] FERNANDEZ M., Math. Struct. in Comp. Science 15 pp 343– (2005) · Zbl 1129.68409 · doi:10.1017/S0960129504004633 [10] FERREIRA H., Analise de Mecanismos para Combinar passos de Beta-Contração em Cálculos de Substituições Explícitas (2005) [11] GUILLAUME B., J. of Func. Programming 10 (4) pp 321– (2000) · Zbl 0971.68021 · doi:10.1017/S0956796800003695 [12] HARDIN T., Algebraic and logic programming, vol. 632 of LNCS pp 306– (1992) · Zbl 0864.90147 · doi:10.1007/BFb0013834 [13] HUET G., TCS 121 pp 145– (1993) · Zbl 0794.03022 · doi:10.1016/0304-3975(93)90087-A [14] KAMAREDDINE F., TCS 155 pp 85– (1996) · Zbl 0873.03018 · doi:10.1016/0304-3975(95)00101-8 [15] KAMAREDDINE F., J. of Func. Programming 7 pp 395– (1997) · Zbl 0882.03011 · doi:10.1017/S0956796897002785 [16] KAMAREDDINE F., Journal of Logic and Computation 10 (3) pp 349– (2000) · Zbl 0953.03013 · doi:10.1093/logcom/10.3.349 [17] KESNER D., TCS 238 (1) pp 183– (2000) · Zbl 0944.68033 · doi:10.1016/S0304-3975(98)00166-2 [18] LIANG C., Rewriting Techniques and Applications (RTA 2002), vol. 2378 of LNCS pp 192– (2002) [19] LIANG C., JAR 33 (2) pp 89– (2004) · Zbl 1102.68019 · doi:10.1007/s10817-004-6885-1 [20] MELLIÈS P.-A., LNCS 902 pp 328– (1995) [21] DE MOURA F. L. C., 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning 3452 pp 433– · doi:10.1007/978-3-540-32275-7_29 [22] NADATHUR G., Proc. 5th Int. Logic Programming Conference pp 810– [23] NADATHUR G., TCS 198 pp 49– (1998) · Zbl 0901.03015 · doi:10.1016/S0304-3975(97)00184-9 [24] NADATHUR G., J. of Func. and Logic Prog. 1999 (2) pp 1– (1999) [25] NADATHUR G., Proceedings Ninth Workshop on Logic, Language, Information and Computation, vol. 67 of ENTCS [26] NADATHUR G., Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming pp 195– [27] NEDERPELT R. P., Selected papers on Automath (1994) [28] RÍOS A., Contribution à l’étude des $$\delta$$-calculs avec substitutions explicites (1993) [29] URBAN C., TCS 323 (1) pp 473– (2004) · Zbl 1078.68140 · doi:10.1016/j.tcs.2004.06.016
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.