Intuitionistic Type Theory is an approach to first-order and higher-order logic, based on a computational justification called the verificationist meaning explanation. First, an untyped and open-ended programming language (also called a computation system) is established with a big-step operational semantics, given by the judgment . Then, a type is defined by specifying how to form a canonical member (“verification”), and when two such canonical members are considered equal. Finally, membership
is evident when
such that
is a canonical member of A.
In this setting, then, the introduction rules follow directly from the defi-nitions of the types, and the elimination rules are explained by showing how one may transform the evidence for their premises into the evidence for their conclusions. For a more detailed exposition of the verificationist meaning explanation for intuitionistic first order logic, see Martin-L¨of (1996); the meaning explanation for full dependent type theory is given in Martin-L¨of (1982) and Martin-L¨of (1984).
1.1 The Connectives of Type Theory
The two main connectives of type theory are the dependent pair (and the dependent function (
, where x may occur free in B.
To define the dependent pair type, we first introduce several new terms into the computation system, together with their canonical forms:
Then, we define the type ((presupposing A type and
B type) by declaring
to be a canonical member under the circumstances that
and
, where [M/x]B stands for the substitution of N for x in B; moreover,
and
are equal canonical members in case
and
.
The formation and introduction rules for dependent pairs are immediately evident by this definition:
The elimination rules for the dependent pair are as follows:
Proof It suffices to validate the elimination rules in case Γ ; then, by hypothesis and inversion of the meaning of membership, we have
such that
and
. By the reduction rule for
) and the meaning of membership,
is immediately evident; because reduction is confluent, we know that [M/x]B is computationally equal to [fst(P)/x]B, whence
becomes evident.
The dependent function type (is defined analogously. First, we augment the computation system with new operators:
Next, we define the type ((presuppose A type and
B type by declaring that
shall be a canonical member under the circumstances that
, and moreover, that
and
shall be equal as canonical members under the circumstances that
.
Just as before, the formation and introduction rules for the dependent function type are immediately evident:
The elimination rule is intended to be the following:
Proof It suffices to consider the case where Γ . By hypothesis, we have that
such that
; then, the reduction rule is applicable, yielding
. By the meaning of hypothetico-general judgment, we may deduce
1.2 Justifying the let Rule
Most programming languages have something called a let expression, which satisfies a rule like the following:
rule for the non-canonical let operator:
Then, the let rule is valid under the meaning explanation.
Proof It suffices to consider the case that Γ . By the meaning of membership under hypothetico-general judgment, we have [
such that
is a canonical member of the type [
1.3 Alternative Meaning Explanations
The standard meaning explanation for type theory is called verificationist because the types are defined by stating how to form a canonical member (i.e. a canonical verification); in this setting, the introduction rules are evident by definition, and the elimination rules must be shown to be locally sound with respect to the introduction rules. This is what we have done above.
An alternative approach is to define a type by its uses, and have the elimination rules be evident by definition; then, the introduction rules must be shown to be locally complete with respect to the elimination rules. This is called the pragmatist meaning explanation.
Finally, following Dummett’s notion of logical harmony, one may choose to explain the connectives by appealing to both their introduction and elimination rules, requiring that they cohere mutually through local soundness and local completeness (Pfenning 2002).
In Dynamic Semantics, the discourse “A man walked in. He sat down.” would be represented by a proposition like the following:
In standard presentations of semantics, of course, the above would be a malformed proposition, because x is out of scope in the right conjunct, however in Dynamic Semantics, the scope of existentials is extended aritificially to make this a well-formed proposition. Following Sundholm’s 1986 revelation, however, in a dependently typed setting we may assign such a sentence the following meaning:
Rather than modifying the behavior of existentials, which under the dependent typing discipline become pairs, we instead use a dependent pair type in place of the conjunction. Conjunctions would become pair types regardless, but by using an explicitly dependent pair, we license the right conjunct to refer to not only the propositional content of the left conjunct, but also to the witnesses of the existentially quantified proposition, by way of projection.
The semantics for a, man, walked in, and sat down are, in simplified form, just direct translations from the usual semantic representations:
Conjunction (in the form of sentence sequencing) is easily assigned a meaning in a similar way:
But when we come to the meaning of the pronoun he, we run into a problem. What could it possibly be? For the example that we are currently considering, we need ), but this is not in general a solution for arbitrary occurrences of the pronoun, since it depends on the name and type of the free variable p.
Consider now the discourse “A man walked in. The man (then) sat down.” The use of the man in the right conjunct, instead of he, introduces presuppositional content via the definite determiner. Ideally, the semantics of this should be nearly identical to those of the previous example (modulo reduction). By giving the a dependently typed meaning, we can achieve this relatively simply:
The first argument to the is simply the predicate, which in this case will be Man. The second argument is an entity, and the third is an inhabitant of the type P x, i.e. a witness that P x holds. Therefore we would want:
The term fst(p) : E is the man referred to in the left conjunct. snd(p) is a witness that he is in fact a man, and that he walked in, and so fst(snd(p)) is the witness that he is a man. The argument fst(p) is, in effect, the solution to the presupposition induced by the, and fst(snd(p)) is the witness that the propositional component of the presupposition holds.
The next two pairs of examples go hand in hand. Consider the classic donkey anaphora sentences “If a farmer owns a donkey, he beats it.” and “Every farmer who owns a donkey beats it.” A typical Dynamic Semantics approach might assign these sentences the following meaning:
In the dependently typed setting, we can assign a similar meaning, but which has a more straightforward connection to the syntax (for convenience, we define the subscript to project the ith element of a right nested tuple):
The lexical entries for the content words and pronouns should be obvious at this point, but for if, a, and every we can define:
With these, we can get:
a farmer owns a donkey
We echo Sundholm’s conclusion that the treatment of donkey-sentences licensed in Martin-L¨of’s type theory is not ad hoc, but rather is reflective of the general suitability of the framework:
In this manner, then, the type-theoretic abstractions suffice to solve the problem of the pronominal back-reference in [the donkey-sentence]. It should be noted that there is nothing ad hoc about the treatment, since all the notions used have been introduced for mathematical reasons in complete independence of the problem posed by [the donkey-sentence]. (Sundholm 1986, p. 503)
2.1 Terms for Presuppositions
Provided that we can devise a general mechanism to assign the meanings given above to pronouns and definite determiners, our semantics will work just as well as standard techniques like Discourse Representation Theory or Dynamic Semantics, but in a well-scoped manner.
A number of possible solutions exist to do precisely this sort of thing in the programming languages literature. Haskell’s type class constraints (Marlow 2010) and Agda’s instance arguments (Devriese and Piessens 2011) provide very similar functionality but for somewhat different purposes, so one option would be to repurpose those ideas.
Haskell’s type classes, however, depend on global reasoning and an antimodular coherence condition which makes them inapplicable to our use-case, since in general there will be many solutions to a presupposition. Agda’s instance arguments are closer to our needs, but we believe that a simpler approach is warranted which lends direct insight into the semantics and pragmatics of presuppositions.
The approach we will take here involves a new operator (require) that binds variables for presupposed parts of an expression. Terms, contexts and signatures are defined as follows:
The new term require x : A in M should be understood to mean roughly “find some x : A and make it available in M.” In this version of type theory, we replace the judgment A type with membership in a universe, ; except where ambiguous, we omit the level from a universe expression, writing Set.
Lexical constants (e.g. Man, Own, etc.) are to be contained in a signature Σ, whereas the context Γ is reserved for local hypotheses. The use of signatures to carry the constants of a theory originates from the Edinburgh Logical Framework, where individual logics were represented as signatures of constants which encode their syntax, judgments and rule schemes (Harper et al 1993; Harper and Licata 2007). Then the basic forms of judgment are as follows:
In context validity judgments , we presuppose
; likewise, in typing judgments Γ
, we presuppose
. The rules for the signature and context validity judgments are as expected:
Constants and hypotheses may be projected from signatures and contexts respectively:
The inference rules for the familiar terms are the usual ones:
The only inference rule which is new deals with presuppositions:
We can now provide a semantics for pronouns and definite determiners:
Now let us reconsider our examples with the new semantics:
2.2 Computational Justification of the require Rule
A require expression is, in essence, the same as a let expression, as found in many programming languages, except that the definiens is supplied by fiat. Its formation rule is a bit strange, of course, because the presupposition’s witness appears in the premises but not in the conclusion; from a type-theoretic perspective, however, this is acceptable.
For instance, many of the rules of Computational Type Theory (Allen et al 2006; Constable et al 1986) strategically forget their premises, yielding novel and useful constructions such as set types {x : A | B(x)} and squash types . On the other hand, this causes the typing judgment to become synthetic (Martin-L¨of 1994): the evidence for the judgment is not recoverable from the statement of the judgment itself, but must be constructed by the knowing subject.
The introduction of types whose members do not contain their own typing derivations is completely justified under the verificationist meaning explanation, but this does not suffice to explain the require rule, which is not part of the definition of a new connective. Intuitionistic validity for require must be established in the same way as the validity of let, i.e. by computation. However, it is clear that we cannot devise an effective operation which produces out of thin air a solution to an arbitrary presupposition if there is one, since this would entail deciding the truth of any proposition (and solving Turing’s Halting Problem).
This, however, does not pose an obstacle for an intuitionistic justification of this rule, since assertion acts are tensed (van Atten 2007). Because evaluation itself is an assertion, we may explain the meaning of the judgment require x : by appealing to the state of knowledge at the time of assertion.
Informally, at time n, the value of require x : A in N shall be, for any witness of that has been experienced by time n, the value of the substitution [M/x]N. It should be noted, then, that the computational behavior of this operator is non-deterministic, since in general the truth of A shall have been experienced in many different ways (corresponding to the number of known solutions to the presupposition).
This explanation suffices to validate the require rule in light of the meaning explanation which was propounded in Section 1:
Proof It suffices to validate the rule in case Γ ; then, we must show that
such that
. By our definition, the require term shall have a value in case a witness for A has been experienced; but this is already the case from the hypothesis
. By inverting the hypothesis [
, we have [
such that
is a canonical member of
This concludes the intuitionistic justification of the require rule.
The augmentation of our computation system with a non-deterministic oracle (require) may be viewed as a computational effect. The behavior of require is defined separately at every type A, and therefore cannot be computed by a recursive algorithm; this “infinitely large” definition is acceptable in type theory because we make no a priori commitment to satisfy Church’s Thesis, which states that every effective operation is recursive. Accepting the possibility of effective but non-recursive operations leads to a property called computational open-endedness (Howe 1991), and endows the intuitionistic continuum with the full richness of the classical one (van Atten 2007).
The explanation of the computational behavior of the require operator is related to the Brouwer’s theory of the Creating Subject, and may be seen as a “proof-relevant” version of Kripke’s Schema. Sundholm explains how the Kreisel-Myhill axiomatization of the Creating Subject may be treated propositionally in Martin-L¨of’s type theory, relative to the existence of a uniform verification object for Kripke’s Schema (Sundholm 2014).
In the same way as we have exploited the intensional character of assertion acts in intuitionistic mathematics, Coquand and Jaber (2012) prove the uniform continuity principle by adding a generic element f to their computation system, representing a Cohen real; their interpretation results in a non-trivial combination of realizability with Beth/Kripke semantics.
Finally, Rahli and Bickford (2015) add two computational effects to type theory (dynamic symbol generation and exception handling), and use them to prove Brouwer’s continuity theorem and justify bar induction on monotone bars.
2.3 Elaboration
In addition to the computational justification of require, we may give a proof-theoretic justification by showing how to eliminate all instances of require from a term via elaboration.To this end, we will define a meta-operation elab(D) which transforms a derivation D :: Γ
into an elaborated term
which is like M but with require expressions replaced by their solutions. We define the operation inductively over the structure of the derivations as follows:
The most crucial rule is the last one — the preceding ones simply define elaboration by induction on the structure of derivations other than those for require expressions. For a require expression, however, we substitute the proof of the presupposed content for the variable in the body of the require expression. It is evident that the elaboration process preserves type.
Theorem 1 Given a derivation D :: Γ , there exists another derivation
:: Γ
) : A.
Proof By induction on the structure of
An example of elaboration in action is necessary, so consider again the sentence “A man walked in. He sat down.” Prior to elaboration, its meaning will be:
Now let Σ = . After constructing a derivation that the above type is a Set under the signature Σ, we can elaborate the associated term. The left conjunct elaborates to itself, so we will not look at that, but the elaboration for the right conjunct is more interesting. The derivation for the right conjunct, letting Γ = p : (
, is:
Inductively, we get:
For the require expression’s elaboration, we substitute fst(p) in for x in x to get the following:
And finally the elaboration of whole subderivation yields SatDown(fst(p)), and so the complete derivation yields
which is the meaning we had wanted.
A similar proof for “A man walked in. The man (then) sat down.” can be given, with an extra non-trivial branch for Man(fst(p)). Focusing just on the subproof for the man, we have the following typing derivation:
This similarly elaborates to fst(p) just as the subproof for he did before.
Elaboration for “If a farmer owns a donkey, he beats it.” and “Every farmer who owns a donkey beats it.” unfolds in a similar fashion, with the elaboration of the antecedent (being trivial. The consequent Beats (require z : E in z) (require w : E in w) breaks down into three subproofs, one for the predicate Beats which elaborates trivially, and the two require subproofs which elaborate like the previous pronominal examples. The only difference now is that the context licenses more options for the proofs.
Keen eyes will notice, however, that there should be four solutions, because both require expressions demand something of type E — the words he and it have no gender distinction in the semantics. This is left as an unspecified part of the framework, as there are a number of options for resolving gender constraints. Two options that are immediately obvious are 1) make E itself a primitive function and then specify a gender appropriately, or 2) add another require expression so that, for example,
) and provide appropriate axioms (possibly simply by deferring to other cognitive systems for judging gender). The former solution is akin to how certain versions of HPSG treat gender as a property of indices not of syntactic elements.
In the previous sections, we have described an approach to pronominal and presuppositional pragmatics based on dependent types, as an alternative to DRT and Dynamic Semantics. The main difference from a standard dependently typed calculus is the addition of require expressions, and an elaboration process to eliminate them.
3.1 Contextual Modal Type Theory
Another approach would be to eliminate require expressions by adopting Contextual Modal Type Theory (CMTT) to support metavariables for presuppositions (Nanevski et al 2008). From our perspective, our system relates to CMTT in the same way that programming directly with computational effects relates to programming in a monad. Indeed, the intuitionistic justification of the require rule obtains by adding an intensional effect to our computation system, whereas a CMTT-based solution would involve solving presuppositions after the fact by providing a substitution.
A modal extension can also provide an interesting solution to another wellknown problem in pragmatics. Consider the sentence “John will pull the rabbit out of the hat” when said of a scene that has 3 rabbits, 3 hats, but only a single rabbit in a hat. This sentence seems to be pragmatically acceptable and unambiguous, despite there being neither a unique rabbit nor a unique hat. In the framework given above, there should be 9 possible ways of resolving the presuppositions, leading to pragmatic ambiguity. A simple modality (approximately a possibility modality), however, can make sense of this: if the assertion of such a sentence presupposes that the sentence can be true via a modality (i.e. to assert P is to presuppose ), then there is only one way to solve the rabbit and hat presuppositions which would also make it possible to resolve the possibility presupposition — pick the rabbit that is in a hat, and the hat that the rabbit is in — yielding a unique, unambiguous meaning. Whether this belongs in the semantics-pragmatics or in some higher system (such as a Gricean pragmatics) is debatable, but that such a simple solution is readily forthcoming at all speaks to the power of the above framework.
3.2 Ranta’s Type-Theoretical Grammar
The most representative use of dependent types in linguistics is Aarne Ranta’s work on type-theoretical grammar (Ranta 1994), where pronominal meaning is given via inference rules for each particular pronoun or other presuppositional form. For example, the pronoun “he” can be explained by giving the following rules:
The first is a typing rule, and the latter is the associated equality rule which reflects computation. This approach can generalize to any sort of presuppositional content, but leaves the question of the meaning of such expressions somewhat unanswered, since these interpretations presuppose that we have already understood the solution to the presupposition.
A discourse context without any possible antecedent will not merely cause a type membership error, as in the system presented in this paper, but will instead not have a meaning at all, as no term can be produced. We consider this an undesirable property in a semantic formalism. Interlocutors will typically not fail to understand sentences with unknown antecedents. For example, when presented with just the sentence “he’s tall” out of the blue, most people will respond by asking “who’s tall?”, rather than by failing to find a meaning at all. To capture this, it’s necessary for the sentence to have a meaning — that is, a term produced by the parser — even in the absence of that meaning computing to a value which the listener shall judge to be a canonical proposition.
In practice, in order to give meanings to anaphora which do not presuppose knowledge of their antecedents, such a theory must be extended with selection operators, such as Bekki’s @-operator (Bekki 2014) or our require operator. This technique, of separating the assignment of meanings from the assertion that they are propositional, is based directly upon Martin-L¨of’s reconstruction of propositional well-formedness as a judgment, rather than a mere matter of grammar (Martin-L¨of 1996).
3.3 Bekki’s @-operator
To assign meanings to anaphora, Bekki (2014) pursued an approach similar to ours, in which an oracle operator (@) was added with the following formation rule:
(@The index i allows an expression to share a presupposition with another, which is a very useful extension that might be added to our framework. Following our computational interpretation of require, we see our operator as essentially a call-by-value analogue to Bekki’s (@
), since in require x : A in N, the presupposition x : A must be resolved before N shall be reduced.
We believe that our require operator is suggestive of the interactive nature of presupposition resolution; indeed, it is possible to see require x : A in N as a dialogue, in which one party requests an A to fill the hole in N — and so it seems likely that the oracle’s choice of a felicitous shall be based in part on the sense of the intended construction N(x), and we may recover the form (@
) as the special case require x : A in x.
Acknowledgements The second author thanks Mark Bickford, Bob Harper and Bob Constable for illuminating discussions on choice sequences, Church’s Thesis, and computational open-endedness. We thank our reviewers for their constructive feedback and references to related work.
Allen S, Bickford M, Constable R, Eaton R, Kreitz C, Lorigo L, Moran E (2006) Innovations in computational type theory using Nuprl. Journal of Applied Logic 4(4):428 – 469, towards Computer Aided Mathematics
Bekki D (2014) Representing anaphora with dependent types. In: Asher N, Soloviev S (eds) Logical Aspects of Computational Linguistics, Lecture Notes in Computer Science, vol 8535, Springer Berlin Heidelberg, pp 14–29
Constable RL, Allen SF, Bromley HM, Cleaveland WR, Cremer JF, Harper RW, Howe DJ, Knoblock TB, Mendler NP, Panangaden P, Sasaki JT, Smith SF (1986) Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., Upper Saddle River, NJ, USA
Coquand T, Jaber G (2012) A computational interpretation of forcing in type theory. In: Dybjer P, Lindstrm S, Palmgren E, Sundholm G (eds) Epistemology versus Ontology, Logic, Epistemology, and the Unity of Science, vol 27, Springer Netherlands, pp 203–213
Devriese D, Piessens F (2011) On the bright side of type classes: Instance arguments in agda. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ACM, New York, NY, USA, ICFP ’11, pp 143–155
Harper R, Licata D (2007) Mechanizing metatheory in a logical framework. Journal of Functional Programming 17(4-5):613–673
Harper R, Honsell F, Plotkin G (1993) A framework for defining logics. Journal of the ACM 40(1):143–184
Howe D (1991) On computational open-endedness in Martin-L¨of’s type theory. In: Logic in Computer Science, 1991. LICS ’91., Proceedings of Sixth Annual IEEE Symposium on, pp 162–172
Marlow S (2010) Haskell 2010 Language Report
Martin-L¨of P (1982) Constructive mathematics and computer programming. In: Cohen LJ, �Lo´s J, Pfeiffer H, Podewski KP (eds) Logic, Methodology and Philosophy of Science VI, Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover 1979, Studies in Logic and the Foundations of Mathematics, vol 104, North-Holland, pp 153–175
Martin-L¨of P (1984) Intuitionistic Type Theory. Bibliopolis
Martin-L¨of P (1994) Analytic and synthetic judgements in type theory. In: Parrini P (ed) Kant and Contemporary Epistemology, The University of Western Ontario Series in Philosophy of Science, vol 54, Springer Netherlands, pp 87–99
Martin-L¨of P (1996) On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic 1(1):11–60
Nanevski A, Pfenning F, Pientka B (2008) Contextual modal type theory. ACM Trans Comput Logic 9(3):23:1–23:49
Pfenning F (2002) Logical frameworks—a brief introduction. In: Schwichtenberg H, Steinbr¨uggen R (eds) Proof and System-Reliability, NATO Science Series, vol 62, Springer Netherlands, pp 137–166
Rahli V, Bickford M (2015) A nominal exploration of intuitionism, unpublished
Ranta A (1994) Type-theoretical Grammar. Oxford University Press, Oxford, UK
Sundholm G (1986) Proof theory and meaning. In: Gabbay D, Guenthner F (eds) Handbook of Philosophical Logic, Synthese Library, vol 166, Springer Netherlands, pp 471–506
Sundholm G (2014) Constructive recursive functions, Church’s Thesis, and Brouwer’s theory of the creating subject: Afterthoughts on a parisian joint session. In: Dubucs J, Bourdeau M (eds) Constructivity and Computability in Historical and Philosophical Perspective, Logic, Epistemology, and the Unity of Science, vol 34, Springer Netherlands, pp 1–35
van Atten M (2007) Brouwer Meets Husserl: On the Phenomenology of Choice Sequences. Springer