Documentation

Linglib.Theories.Interfaces.SyntaxSemantics.Minimalism.TopologicalMapping

The Topological Mapping Theory #

@cite{longobardi-2005} @cite{longobardi-1994}

@cite{longobardi-2005} §9: a mapping theory from nominal syntactic forms to logically oriented representations. The theory rests on two axioms and a licensing condition, from which the Core Generalization — reference (to individuals) iff N-to-D — follows as a theorem.

Axioms #

Derived Theorems #

Noun Taxonomy #

Four classes of nominal heads, ranked by three diagnostic tests: object-referentiality, predicative restrictions, and kind-referentiality.

source
inductive Interfaces.SyntaxSemantics.TopologicalMapping.NominalHeadClass :
Type

The four classes of nominal heads, ranked from most prototypically referential (pronouns) to least (common nouns).

@cite{longobardi-2005} table (28): these four classes are distinguished by three tests — object-referentiality (in D), predicative restrictions (not in D), and kind-referentiality (with definite article).

  • pronoun : NominalHeadClass

    Always in D in all argument environments. Object-referential only. Cannot function predicatively or as kind-denoting expressions.

  • properName : NominalHeadClass

    Raise to D obligatorily in argument function (Romance). Object-referential. Predicative use conditioned. No kind reading.

  • specialCommon : NominalHeadClass

    Raise to D only under special conditions (genitive modifier, deictic context). Object-referential when raised. Full predicative use. Kind-referential with definite article. Examples: casa 'home', mamma 'mom', lunedì 'Monday'.

  • commonNoun : NominalHeadClass

    Never raise to D. Never object-referential. Full predicative use. Kind-referential with definite article.

Instances For
    source
    instance Interfaces.SyntaxSemantics.TopologicalMapping.instDecidableEqNominalHeadClass :
    DecidableEq NominalHeadClass
    Equations
    source
    def Interfaces.SyntaxSemantics.TopologicalMapping.instReprNominalHeadClass.repr :
    NominalHeadClass → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Interfaces.SyntaxSemantics.TopologicalMapping.instReprNominalHeadClass :
      Repr NominalHeadClass
      Equations
      source
      def Interfaces.SyntaxSemantics.TopologicalMapping.instBEqNominalHeadClass.beq :
      NominalHeadClass → NominalHeadClass → Bool
      Equations
      Instances For
        source
        instance Interfaces.SyntaxSemantics.TopologicalMapping.instBEqNominalHeadClass :
        BEq NominalHeadClass
        Equations
        source
        def Interfaces.SyntaxSemantics.TopologicalMapping.objectReferential :
        NominalHeadClass → Bool

        Object-referential: the nominal can denote a specific object (individual in Carlson's sense) by occupying the D position.

        Equations
        Instances For
          source
          def Interfaces.SyntaxSemantics.TopologicalMapping.canBePredicate :
          NominalHeadClass → Bool

          Can function as a predicate (i.e., survive without D).

          Equations
          Instances For
            source
            def Interfaces.SyntaxSemantics.TopologicalMapping.kindReferential :
            NominalHeadClass → Bool

            Kind-referential: can denote a kind when introduced by definite article.

            Equations
            Instances For
              source
              def Interfaces.SyntaxSemantics.TopologicalMapping.raisingObligatory :
              NominalHeadClass → Bool

              Whether N-to-D raising is obligatory in argument position.

              Equations
              Instances For
                source
                theorem Interfaces.SyntaxSemantics.TopologicalMapping.table_28 :
                objectReferential NominalHeadClass.pronoun = true ∧ objectReferential NominalHeadClass.properName = true ∧ objectReferential NominalHeadClass.specialCommon = true ∧ objectReferential NominalHeadClass.commonNoun = false ∧ kindReferential NominalHeadClass.pronoun = false ∧ kindReferential NominalHeadClass.properName = false ∧ kindReferential NominalHeadClass.specialCommon = true ∧ kindReferential NominalHeadClass.commonNoun = true ∧ canBePredicate NominalHeadClass.pronoun = false ∧ canBePredicate NominalHeadClass.properName = true ∧ canBePredicate NominalHeadClass.specialCommon = true ∧ canBePredicate NominalHeadClass.commonNoun = true

                Table (28): the three diagnostics partition the four classes. Pronouns and proper names are object-referential but not kind-referential. Special common nouns and common nouns are kind-referential but differ in object-referentiality.

                source
                def Interfaces.SyntaxSemantics.TopologicalMapping.propernessRank :
                NominalHeadClass → ℕ

                The scalar hierarchy of properness from @cite{longobardi-2005} (25).

                Nominal expressions are ranked along a scale from most prototypically proper-like to most common-like. Access to the N-to-D derivational strategy decreases monotonically along this scale.

                a. Pronouns: always in D. b. Names of persons, geographical units: raise whenever D is empty. c. Names of days: raise only under particular semantic conditions. d. Casa, kinship terms: raise only if followed by genitive modifier. e. Normal common nouns: never raise.

                Equations
                Instances For
                  source
                  theorem Interfaces.SyntaxSemantics.TopologicalMapping.raising_monotone (c₁ c₂ : NominalHeadClass) :
                  propernessRank c₁ ≤ propernessRank c₂ → raisingObligatory c₂ = true → raisingObligatory c₁ = true

                  Raising access decreases monotonically with properness rank: if class c₁ is more proper than c₂, then c₁'s raising is at least as obligatory as c₂'s.

                  source
                  inductive Interfaces.SyntaxSemantics.TopologicalMapping.LexicalNamingType :
                  Type

                  The lexical type of a noun: whether it names objects or kinds.

                  @cite{longobardi-2005} §4: nouns lexically divide into object-naming (proper names, pronouns — intrinsically referential) and kind-naming (common nouns — denote kinds, not individuals).

                  • objectNaming : LexicalNamingType

                    Object-naming: learning the name means learning to apply it to a particular object. Proper names, pronouns.

                  • kindNaming : LexicalNamingType

                    Kind-naming: learning the name means learning to recognize a potentially open set of objects. Common nouns.

                  Instances For
                    source
                    instance Interfaces.SyntaxSemantics.TopologicalMapping.instDecidableEqLexicalNamingType :
                    DecidableEq LexicalNamingType
                    Equations
                    source
                    instance Interfaces.SyntaxSemantics.TopologicalMapping.instReprLexicalNamingType :
                    Repr LexicalNamingType
                    Equations
                    source
                    def Interfaces.SyntaxSemantics.TopologicalMapping.instReprLexicalNamingType.repr :
                    LexicalNamingType → ℕ → Std.Format
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Interfaces.SyntaxSemantics.TopologicalMapping.instBEqLexicalNamingType.beq :
                      LexicalNamingType → LexicalNamingType → Bool
                      Equations
                      Instances For
                        source
                        instance Interfaces.SyntaxSemantics.TopologicalMapping.instBEqLexicalNamingType :
                        BEq LexicalNamingType
                        Equations
                        source
                        structure Interfaces.SyntaxSemantics.TopologicalMapping.NominalConfig :
                        Type

                        A nominal argument configuration, capturing the syntactic and semantic state of a DP in argument position.

                        • namingType : LexicalNamingType

                          The head noun's lexical naming type

                        • dHasReferentialContent : Bool

                          Does D contain a lexically referential expression? (either an overt determiner/quantifier, or N raised to D, or an expletive article linked to a raised N in a CHAIN)

                        • isArgument : Bool

                          Is the nominal in argument function?

                        Instances For
                          source
                          instance Interfaces.SyntaxSemantics.TopologicalMapping.instDecidableEqNominalConfig :
                          DecidableEq NominalConfig
                          Equations
                          source
                          def Interfaces.SyntaxSemantics.TopologicalMapping.instDecidableEqNominalConfig.decEq (x✝ x✝¹ : NominalConfig) :
                          Decidable (x✝ = x✝¹)
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            instance Interfaces.SyntaxSemantics.TopologicalMapping.instReprNominalConfig :
                            Repr NominalConfig
                            Equations
                            source
                            def Interfaces.SyntaxSemantics.TopologicalMapping.instReprNominalConfig.repr :
                            NominalConfig → ℕ → Std.Format
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def Interfaces.SyntaxSemantics.TopologicalMapping.instBEqNominalConfig.beq :
                              NominalConfig → NominalConfig → Bool
                              Equations
                              Instances For
                                source
                                instance Interfaces.SyntaxSemantics.TopologicalMapping.instBEqNominalConfig :
                                BEq NominalConfig
                                Equations
                                source
                                def Interfaces.SyntaxSemantics.TopologicalMapping.denotesIndividual (nc : NominalConfig) :
                                Bool

                                (52) Denotation Hypothesis: Individuals are denoted in D.

                                The D position is the locus of referential interpretation. A nominal denotes an individual (object or kind) iff its D position is associated with referential content.

                                Equations
                                Instances For
                                  source
                                  def Interfaces.SyntaxSemantics.TopologicalMapping.argumentLicensed (nc : NominalConfig) :
                                  Bool

                                  (53) Licensing Condition: Arguments denote individuals.

                                  Full Interpretation requires arguments to have a referential value (whether constant or variable).

                                  Equations
                                  Instances For
                                    source
                                    def Interfaces.SyntaxSemantics.TopologicalMapping.isConstant (nc : NominalConfig) :
                                    Bool

                                    (54a) A constant: a fixed referential value denoting one and only one entity (kind or object). Requires D to contain (or CHAIN-link to) a lexically referential expression — either a raised N, an overt determiner, or a pronoun base-generated in D.

                                    Equations
                                    Instances For
                                      source
                                      def Interfaces.SyntaxSemantics.TopologicalMapping.isVariable (nc : NominalConfig) :
                                      Bool

                                      (54b) A variable: bound by an operator (existential, generic, or the variable-binding force of a lexical determiner) and ranging over a set of entities. Arises when D is empty (no referential content).

                                      Equations
                                      Instances For
                                        source
                                        theorem Interfaces.SyntaxSemantics.TopologicalMapping.empty_d_arguments_are_variables (nc : NominalConfig) (_hArg : nc.isArgument = true) (hEmptyD : nc.dHasReferentialContent = false) :
                                        isVariable nc = true

                                        (55) Arguments with empty D are variables.

                                        From (52)+(53)+(54): if D is empty, then by (52) the nominal cannot denote an individual via D. By (53) it must still denote (being an argument). By (54b) the only remaining option is variable interpretation.

                                        source
                                        theorem Interfaces.SyntaxSemantics.TopologicalMapping.constant_requires_d_content (nc : NominalConfig) (hConst : isConstant nc = true) :
                                        nc.dHasReferentialContent = true

                                        (56) An argument is a constant only if D contains a lexically referential expression.

                                        Equivalently: constant interpretation requires N-to-D (for proper names), an overt determiner, or a pronoun in D.

                                        source
                                        theorem Interfaces.SyntaxSemantics.TopologicalMapping.core_generalization (nc : NominalConfig) :
                                        isConstant nc = true ↔ nc.dHasReferentialContent = true

                                        (33) The Core Generalization: Reference (to individuals) iff N-to-D.

                                        This is the paper's central result, unifying object reference and kind reference. A nominal refers to an individual (constant interpretation) if and only if D has referential content (achieved by N-to-D raising for proper names, by an overt determiner for common nouns, or by base-generation for pronouns).

                                        source
                                        theorem Interfaces.SyntaxSemantics.TopologicalMapping.argument_requires_d (nc : NominalConfig) (hArg : nc.isArgument = true) (hLicensed : argumentLicensed nc = true) :
                                        denotesIndividual nc = true

                                        (41) A nominal is an argument only if introduced by D.

                                        @cite{longobardi-2005} §7: this principle, from @cite{szabolcsi-1987} and @cite{stowell-1989-1991}, is derived from (52)+(53). In non-argument environments (predicates, vocatives, exclamations), nominals can occur without D.

                                        source
                                        theorem Interfaces.SyntaxSemantics.TopologicalMapping.proper_names_must_raise (nc : NominalConfig) :
                                        nc.namingType = LexicalNamingType.objectNaming → nc.isArgument = true → argumentLicensed nc = true → nc.dHasReferentialContent = true

                                        @cite{longobardi-2005} §10, question (57c): Why must proper names raise?

                                        Object-naming nouns cannot satisfy (54b) — they name objects, not kinds, so they cannot enter the interpretive formula Dx.x ∈ kind(N) that gives variables their meaning. Their only route to argumenthood is constant interpretation via (54a), which requires D content. Since proper names are bare (no overt determiner), they must raise N-to-D to fill D.

                                        source
                                        theorem Interfaces.SyntaxSemantics.TopologicalMapping.common_nouns_need_not_raise (nc : NominalConfig) :
                                        nc.namingType = LexicalNamingType.kindNaming → nc.isArgument = true → nc.dHasReferentialContent = false → isVariable nc = true

                                        @cite{longobardi-2005} §10, question (57a): Why do common nouns not have to raise?

                                        Kind-naming nouns can satisfy (54b): they name kinds, so they can enter the formula Dx.x ∈ kind(N) as the restrictor of a variable. Empty D yields a variable bound by an existential or generic operator. No raising is needed for convergence.

                                        source
                                        inductive Interfaces.SyntaxSemantics.TopologicalMapping.ArticleType :
                                        Type

                                        Whether a definite article is expletive (semantically vacuous placeholder) or a genuine semantic operator.

                                        @cite{longobardi-2005} §8: when a proper name appears with a definite article (la Maria, il Gianni), the article is expletive — it does not contribute uniqueness or familiarity semantics. It merely fills the D position that N-raising would otherwise occupy.

                                        • expletive : ArticleType

                                          Expletive: phonological placeholder for D, no semantic content. Forms a CHAIN with the noun. la Maria ≈ Maria raised to D.

                                        • operator : ArticleType

                                          Semantic operator: contributes uniqueness (ι), familiarity, or quantificational force. il tavolo 'the table' — real definite.

                                        Instances For
                                          source
                                          instance Interfaces.SyntaxSemantics.TopologicalMapping.instDecidableEqArticleType :
                                          DecidableEq ArticleType
                                          Equations
                                          source
                                          instance Interfaces.SyntaxSemantics.TopologicalMapping.instReprArticleType :
                                          Repr ArticleType
                                          Equations
                                          source
                                          def Interfaces.SyntaxSemantics.TopologicalMapping.instReprArticleType.repr :
                                          ArticleType → ℕ → Std.Format
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            def Interfaces.SyntaxSemantics.TopologicalMapping.instBEqArticleType.beq :
                                            ArticleType → ArticleType → Bool
                                            Equations
                                            Instances For
                                              source
                                              instance Interfaces.SyntaxSemantics.TopologicalMapping.instBEqArticleType :
                                              BEq ArticleType
                                              Equations
                                              source
                                              def Interfaces.SyntaxSemantics.TopologicalMapping.expletiveBlocksKindReading :
                                              ArticleType → Bool

                                              An expletive article does not induce kind readings.

                                              @cite{longobardi-2005} (46)–(47): la Maria behaves identically to bare Maria — wide scope, rigid, no generic/kind reading. This distinguishes expletive articles from genuine definite operators, which CAN induce kind readings (i cani 'the dogs' = the dog-kind).

                                              Equations
                                              Instances For
                                                source
                                                theorem Interfaces.SyntaxSemantics.TopologicalMapping.proper_name_in_d_is_constant {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) :
                                                Semantics.Reference.Basic.isDirectlyReferential (Semantics.Reference.Basic.properName e).character ∧ Semantics.Reference.Basic.constantCharacter (Semantics.Reference.Basic.properName e).character

                                                Proper names in D are directly referential.

                                                Bridge connecting the syntactic analysis (N-to-D raising creates constant interpretation) to the semantic analysis (proper names have constant character and rigid content). The two perspectives converge: syntactically, D is the locus of reference; semantically, proper names are rigid designators.