Abstract
In Transparent Intensional Logic we can recognize two distinct notions of computation that loosely correspond to term rewriting and term interpretation as known from lambda calculus. Our goal will be to further explore these two notions and examine some of their properties.
Similar content being viewed by others
Notes
Note the difference between \({\mathbf{1}}\) and 1, which will be explained below.
See e.g., Barendregt (1984).
See e.g., Raclavský et al. (2015, p. 255).
The from left to right interpretation is also followed by Moschovakis (2006), Muskens (2005), Girard et al. (1989). The from right to left interpretation is explored e.g., in Martin-Löf’s constructive type theory (CTT, see Martin-Löf 1984). For a comparison between CTT and TIL, see e.g., Pezlar (2017), Primiero and Jespersen (2010).
Traditionally, TIL is equipped with single execution, double execution and trivialisation construction. The notion of n-execution is a generalization of these constructions, see “Appendix 1”.
0-execution, i.e., zero execution, has many uses in TIL, one of them being introduction of pre-defined objects into TIL constructions. From this perspective, we can view 0-executions as analogous to constants in impure lambda calculus.
For a proper specification of all constructions, see “Appendix 1”.
See “Appendix 1”, def. 8 for the specification of \(\beta \)-reduction.
Let us not confuse \([x \; y]\) with “apply variable x to variable y”, the proper reading should be “apply the function v-constructed by variable x to the argument v-constructed by variable y”.
By “modulo 0-execution” we simply mean ignoring the outermost 0-execution. For example, \({{\mathbf{12}}}\) modulo 0-execution becomes 12 (recall that \({{\mathbf{12}}}\) is a shorthand for \(^012\)).
For simplicity, we consider only compositions composed of two constructions, one constructing a function, the other its argument.
An alternative formulation can be found in Raclavský et al. (2015).
We utilize \(\beta \)-reduction by name (see Duží 2017). Although there are known instances where this rule fails to preserve strict equivalence between constructions, this doesn’t need to concern us here, since the main argument of this paper holds even for variants of \(\beta \)-reduction preserving strict equivalence (e.g., restricted \(\beta \)-reduction by name).
For more about ramified type hierarchy, see Sect. 2.
References
Barendregt Hendrik P (1984) The lambda calculus: its syntax and semantics. North-Holland, Amsterdam
Duží M (2017) If structured propositions are logical procedures then how are procedures individuated? Synthese. https://doi.org/10.1007/s11229-017-1595-5 (in press)
Duží M, Kosterec M (2017) A valid rule of \(\beta \)-conversion for the logic of partial functions. Organon F 24(1):10–36
Duží M, Jespersen B, Materna P (2010) Procedural semantics for hyperintensional logic: foundations and applications of transparent intensional logic. Springer, Dordrecht
Girard J-Y, Taylor P, Lafont Y (1989) Proofs and types. Cambridge University Press, Cambridge
Jespersen B (2017) Anatomy of a proposition. Synthese. https://doi.org/10.1007/s11229-017-1512-y (in press)
Martin-Löf P (1984) Intuitionistic type theory. Bibliopolis, Berkeley
Materna P (1998) Concepts and objects. Philosophical Society of Finland, Helsinki
Materna P (2013) Equivalence of problems (an attempt at an explication of problem). Axiomathes 23(4):617–631. https://doi.org/10.1007/s10516-012-9201-4
Moschovakis YN (2006) A logical calculus of meaning and synonymy. Linguist Philos 29(1):27–89. https://doi.org/10.1007/s10988-005-6920-7
Muskens R (2005) Sense and the computation of reference. Linguist Philos 28(4):473–504. https://doi.org/10.1007/s10988-004-7684-1
Pezlar I (2017) Algorithmic theories of problems. A constructive and a non-constructive approach. Log Log Philos 26(4):473–508. https://doi.org/10.12775/LLP.2017.010
Primiero G, Jespersen B (2010) Two kinds of procedural semantics for privative modification. Lect Notes Artif Intell 6284:251–271
Raclavský J (2003) Executions vs. constructions. Logica et Methodologica 7:63–72
Raclavský J, Kuchyňka P, Pezlar I (2015) Transparentní intenzionální logika jako characteristica universalis a calculus ratiocinator. Masaryk University Press (Munipress), Brno
Sierszulska A (2006) On Tichý’s determiners and Zalta’s abstract objects. Axiomathes 16(4):486–498. https://doi.org/10.1007/s10516-006-0002-5
Tichý P (1988) The foundations of Frege’s logic. de Gruyter, Berlin
van Heijenoort J (1977) From Frege to Gödel: a source book in mathematical logic, 1879–1931. Harvard University Press, Cambridge
Acknowledgements
An earlier version of this paper was presented at the 21st Conference Applications of Logic in Philosophy and the Foundations of Mathematics in Szklarska Porȩba, Poland 2016. I would like to thank all the participants of this conference for their valuable notes and remarks.
Author information
Authors and Affiliations
Corresponding author
Additional information
Work on this paper was supported by Grant No. 17-18344Y from the Czech Science Foundation, GA ČR.
Appendix
Appendix
1.1 Constructions
The traditional definition of TIL constructions goes as follows (original formulation by Tichý 1988, we follow Duží et al. 2010 with minor deviations):Footnote 17
Definition 5
(Constructions)
-
1.
The variablex is a construction that constructs an object O of the respective type dependently on a valuation. We say that it v-constructs O.
-
2.
Where X is any object, \(^0 X\) is the construction trivialization. It constructs X without any change.
-
3.
The composition\([X_0 \, X_1 \ldots X_m]\) is the following construction. If Xv-constructs a function f of type \((\alpha \beta _1 \ldots \beta _m)\) and \(X_1 \ldots X_m\)v-construct objects \(b_1 , \ldots , b_m\) of types \(\beta _1 , \ldots , \beta _m\), respectively, then the composition\([X_0 \, X_1 \ldots X_m]\)v-constructs the value (an object of type \(\alpha \), if any) of f on the tuple-argument \(\langle b_1 , \ldots ,b_m \rangle \). Otherwise, it is a v-improperconstruction, i.e., construction that does not construct anything.
-
4.
The closure\([\lambda x_1 \ldots x_m \, Y]\) is the following construction. Let \(x_1 , \ldots x_m\) be pairwise distinct variables v-constructing objects of types \(\beta _1 , \ldots , \beta _m\) and Y a construction v-constructing an object of type \(\alpha \). Then \([\lambda x_1 \ldots x_m \, Y]\) is the constructionclosure. It v-constructs the following function f of type \((\alpha \beta _1 \ldots \beta _m)\): let \(\langle b_1, \ldots , b_m \rangle \) be a tuple of objects of types \(\beta _1 \ldots \beta _m\), respectively, and \(v'\) be a valuation that associates \(x_i\) with \(b_i\) and is identical to v otherwise. Then the value of function f on argument tuple \(\langle b_1, \ldots , b_m \rangle \) is the object of type \(\alpha \)\(v'\)-constructed by Y. If Y is \(v'\)-improper, then f is undefined on \(\langle b_1, \ldots , b_m \rangle \).
-
5.
The single execution\(^1 X\) is the construction that either v-constructs the object v-constructed by X or, if Xv-constructs nothing, is v-improper.
-
6.
The double execution\(^2 X\) is the following construction: let X be any object, the double execution\(^2 X\) is v-improper if X is a non-construction or if X does not v-construct a construction or if Xv-constructs a v-improper construction. Otherwise, let Xv-construct a construction \(X'\) and let \(X'\)v-construct and object \(X''\), then \(^2 K\)v-constructs \(X''\).
-
7.
Nothing other is a construction, unless it follows from 1–6.
1.2 Ramified Type Theory
We follow the specification from Tichý (1988):
Definition 6
(Ramified type theory of TIL)
Let B be a base, i.e., a set of atomic types.
-
1.
-
(\(\hbox{t}_1\)i) Every member of B is a type of order 1 over B.
-
(\(\hbox{t}_1\)ii) If \(0<m\) and \(\alpha , \beta _1 \ldots \beta _m\) are types of order 1 over B, then the collection \((\alpha \beta _1 \ldots \beta _m)\) of all m-ary (total and partial) mappings from \(\beta _1 \ldots \beta _m\) to \(\alpha \) is also a type of order 1 over B.
-
(\(\hbox{t}_1\)iii) Nothing is a type of order 1 over B unless it follows from (\(\hbox{t}_1\)i) and (\(\hbox{t}_1\)ii).
-
-
2.
-
(\(\hbox{c}_k\)i) Let \(\alpha \) be any type of orderkover B. Every variable ranging over \(\alpha \) is a construction of order k over B. If X is of (i.e., belongs to) type \(\alpha \), then \(^0 X\), \(^1 X\), and \(^2 X\) are constructions of order k over B. Every variable ranging over \(\alpha \) is a construction of orderkover B.
-
(\(\hbox{c}_k\)ii) If \(0<m\) and \(X_0, X_1, \ldots , X_m\) are constructions of orderk, then \([X_0 \; X_1 \ldots \, X_m]\) is a construction of order k over B. If \(0<m\), \(\alpha \) is a type of orderkover B, and Y as well as the distinct variables \(x_1, \ldots , x_m\) are constructions of orderkover B, then \([\lambda _\alpha \, x_1 \ldots x_m \; Y]\) is a construction of orderkover B.
-
(\(\hbox{c}_k\)iii) Nothing is a construction of orderkover B unless it follows from (\(\hbox{c}_k\)i) and (\(\hbox{c}_k\)ii).
-
Let \(*_k\) be the collection of constructions of order k over B. The collection of types of order\(k+1\)over B is defined as follows:
-
(\(\hbox{t}_{k+1}\)i) \(*_n\) and every type of order n is a type of order\(k+1\).
-
(\(\hbox{t}_{k+1}\)ii) If \(0<m\) and \(\alpha , \beta _1 , \ldots , \beta _m\) are types of order\(k+1\)over B, then the collection \((\alpha \beta _1 \ldots \beta _m)\) of all m-ary (total and partial) mappings from \(\beta _1 , \ldots , \beta \) to \(\alpha \) is also a type of order\(k+1\)over B.
-
(\(\hbox{t}_{k+1}\)iii) Nothing is a type of order\(k+1\)over B unless it follows from (\(\hbox{t}_{k+1}\)i) and (\(\hbox{t}_{k+1}\)ii).
1.3 Collisionless Substitution
Originally defined by Duží et al. (2010):
Definition 7
(Collisionless substitution) Let x be a variable and C, D any kinds of construction. If x is not free in C, then the result of substitutingDforxinC is C. Assume now that x is free in C. Then:
-
(a)
If C is x, then the result of substitutingDforxinC is D. If C is \(^1 X\) or \(^2 X\), then the result of substitutingDforxinC is \(^1 Y\) or \(^2 Y\), where Y is the result of substituting D for x in X.
-
(b)
If C is \([X \, X_1 \ldots X_m]\), then the result of substitutingDforxinC is \([Y \, Y_1 \ldots Y_m]\), where \(Y , Y_1 , \ldots , Y_m\) are the results of substituting D for x in \(X , X_1 , \ldots , X_m\), respectively.
-
(c)
Let C be of the form \([\lambda x_1 \ldots x_m \, Y]\); for \(1 \le i \le m\), let \(y_i = x_i\) if \(x_i\) is not free in D, and otherwise the first variable v-constructing entities of the same type as \(x_i\), not occurring in C, not free in D, and distinct from \(y_1 , \ldots , y_{i+1}\). Then the result of substitutingDforxinC is \([\lambda y_1 \ldots y_m \, Z]\), where Z is the result of substituting D for x in the result of substituting \(y_i\) for \(x_i(1 \le i \le m)\) in Y.
To simplify the notation, let \(C, D_1 , \ldots , D_n \) be arbitrary constructions, \(x_1 , \ldots , x_n\) variables. Then, for \(1 \le i \le n\), \(C(D_i/x_i)\) will represent the result of substituting \(D_i\) for \(x_i\) in C.
1.4 \(\beta \)-Reduction
We follow the specification of \(\beta \)-reduction from Duží (2017):Footnote 18
Definition 8
(\(\beta \)-reduction) Let C be a construction typed to v-construct object of type \(\alpha \), \(x_1\) and \(D_1\) constructions typed to v-construct objects of type \(\beta _1\), ..., \(x_n\) and \(D_n\) constructions typed to v-construct objects of type \(\beta _n\) and \([\lambda x_1 \ldots x_n \, C]\) is typed to v-construct object of type \((\alpha \beta _1 \ldots \beta _n )\), then
where \(C(D_1 / x_1 \ldots D_n / x_n)\) is the construction that arises from C by collisionless substitution of \(D_1\) for all the occurrences of \(x_1\), ..., \(D_n\) for all the occurrences of \(x_n\).
1.5 n-Execution
In this section, we introduce the construction of multiple execution we will call n-execution (for \(n \ge 0\)), which is a generalization of TIL’s native constructions execution and double execution (see Sect. 1 above). Further, we will show that trivialization can be understood as its limiting case when \(n = 0\). Our generalization is based on the following three simple observations that keep reappearing in TIL literature:
Observation 1
Intuitively, if we have single execution and double execution, then we should be able to consider even triple execution, quadruple execution and so on. And if that is the case, then we can generalize this observation and introduce the notion of n-execution where n is the number of consecutive executions.Footnote 19
Observation 2
If we should understand \(^1 X\) as ‘execute X’ (i.e., ‘\(^1\)’ = one execution) and \(^2 X\) as ‘execute X and then execute its result \(X'\)’ (i.e., ‘\(^2\)’ = two executions), then, arguably the most natural reading of \(^0 X\)—if we have never heard of trivialization—is ‘do not execute \(X'\) (i.e., ‘\(^0\)’ = zero executions).Footnote 20
Observation 3
Multiple execution for \(n > 2\) is reducible to iterated double execution.Footnote 21
Definition 9
(n-execution) For any object X we shall speak of the n-execution of X and symbolize it as \(^n X\), where \(n \ge 0\).
-
1.
If \(n = 0\), then \(^0 X\) is X (where X is either a construction or a non-construction). More specifically, to carry out \(^0 X\), we start with X and do nothing further with it, not even valuation. It is never v-improper.
-
2.
If \(n \ge 1\), there is a need to distinguish two main cases (the second has three further subcases):
-
(a)
X is a non-construction: then \(^n X\) is v-improper construction.
-
(b)
X is a construction:
-
i.
n = 1: then nXv-constructs the same object as does X (if any).
-
ii.
n = 2: then nXv-constructs the object v-constructed by X′ (assuming nXv-constructs X′). Otherwise, it is v-improper.
-
iii.
n > 2: then nXv-constructs the same object (if any) as does sX where s is a sequence of n − 1 iterated n-executions with n = 2. For example, 3X can be reduced to 2(2X).
-
i.
-
(a)
From the type-theoretical perspective, if X is of (i.e., belongs to) some type \(\alpha \) of order k over B, then \(^n X\) (where \(n \ge 0\)) is a construction of orderkover B.Footnote 22
To get a better feeling of how n-execution works for cases with \(n > 1\), consider the following cases:
-
1.
\(n = 2\): same as Tichý’s original definition above.
-
2.
\(n = 3\): analogously to the case above, but the construction \(X'\)v-constructed by X has to be v-constructing another (proper) construction \(X''\), otherwise it is v-improper.
-
3.
\(n = 4\): analogously to the case above, but \(X''\) has to be v-constructing yet another (proper) construction \(X'''\), otherwise it is v-improper.
... etc.
Specific instances of n-execution (for \(n = 0, 1 , 2, \ldots \)) will be called 0-execution, 1-execution, 2-execution, etc. For example, \(^0 5\) is an example of 0-execution, \(^1 x\) is an example of 1-execution, \(^2 5\) is an example of 2-execution, etc.
To conclude, on this approach, trivialization, execution, and double execution are just specific instances of n-execution for some \(n \ge 0\), with trivialization being an alternative name for the degenerate case when \(n = 0\) (informally: ‘do not execute’, ‘do nothing’ or—as Tichý put it—‘leave it as it is’ (Tichý 1988, p. 63).
Remark 7
The case of \(n = 0\) is a special one also from another point of view – the appearance of ‘\(^0\)’, i.e., 0-execution, binds free variables in contrast to 1-execution, 2-execution, etc. (see e.g., Duží et al. 2010, p. 47). As we mentioned, 0-execution \(^0 X\) is essentially an instruction to ‘do nothing with X’ and by binding the free variables we are making sure that nothing is indeed done with X, not even valuation or substitution.
Rights and permissions
About this article
Cite this article
Pezlar, I. On Two Notions of Computation in Transparent Intensional Logic. Axiomathes 29, 189–205 (2019). https://doi.org/10.1007/s10516-018-9401-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10516-018-9401-7