Generalizations.Projectivity — cross-paper data pool #

The Gradient Projection Principle of [TBD18] — content projects to the extent that it is not at-issue — predicts a per-expression projectivity from its at-issueness. This file is the theory-neutral pool against which rival accounts of that relationship are run.

The empirical generalisation (projectivity is gradient and tracks not-at-issueness across triggers) predates any one formal account and spans ≥ 2 papers contributing generated Data.Examples rows ([TBD18]: 9 + 12 English expressions; [SB24]: occasion + psychological verbs in German), with ≥ 2 rival accounts run against the pool in their study files (gppProjection and pottsProjection in Studies/TonhauserBeaverDegen2018).

Main declarations #

ProjectionDatum — a typed observed datum (projectivity, atIssueness), lifted from a paper-anchored LinguisticExample by fromExample.
allData — the pooled test set: every projectivity row from the contributing papers' generated Examples.all.
predictionError / predictsWithin — score an account against an observation.

Implementation notes #

The means are continuous (proportions in [0, 1]), so an account is run over allData by computation; the kernel-checkable content is each account's systematic error, proved in the study files (string-keyed paperFeatures and ℚ comparison do not reduce in the kernel). Papers may store either atIssueness or notAtIssueness in paperFeatures; readAtIssueness normalises both to at-issueness (the accounts' input). Import rule (Core + Data only): accounts and divergence theorems live in the consuming study files.

source

structure Generalizations.Projectivity.ProjectionDatum :

Type

An observed datum: mean projectivity and at-issueness for one expression, with its originating SourceRef.

expression : String
projectivity : ↑(Set.Icc 0 1)
atIssueness : ↑(Set.Icc 0 1)
source : Data.Examples.SourceRef

Instances For

source

def Generalizations.Projectivity.ProjectionDatum.notAtIssueness (d : ProjectionDatum) :

↑(Set.Icc 0 1)

Not-at-issueness is the complement of at-issueness — the quantity the GPP equates with projectivity.

Equations

d.notAtIssueness = Set.Icc.symm d.atIssueness

Instances For

`LinguisticExample` adapter #

source

def Generalizations.Projectivity.parsePercent (s : String) :

Option ↑(Set.Icc 0 1)

Parse a percent-integer string (e.g. "96") into Set.Icc (0 : ℚ) 1; none if non-numeric or out of range.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Generalizations.Projectivity.readAtIssueness (pf : List (String × String)) :

Option ↑(Set.Icc 0 1)

Read at-issueness from paperFeatures: directly from the atIssueness key, or as the complement of notAtIssueness.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Generalizations.Projectivity.fromExample (e : Data.Examples.LinguisticExample) :

Option ProjectionDatum

Lift a LinguisticExample to a ProjectionDatum via its expression, projectivity, and (atIssueness or notAtIssueness) keys; none if any is missing.

Equations

One or more equations did not get rendered due to their size.

Instances For

Pool #

source

def Generalizations.Projectivity.allData :

List ProjectionDatum

The pooled cross-paper projection data. Each rival account — a map from at-issueness to predicted projectivity on Set.Icc (0 : ℚ) 1 — is run against this list in the study files.

Equations

Generalizations.Projectivity.allData = List.filterMap Generalizations.Projectivity.fromExample (TonhauserBeaverDegen2018.Examples.all ++ SolstadBott2024.Examples.all)

Instances For

Scoring #

source

def Generalizations.Projectivity.predictionError (acc : ↑(Set.Icc 0 1) → ↑(Set.Icc 0 1)) (d : ProjectionDatum) :

ℚ

An account's absolute error on an observation: the gap between its predicted projectivity (from the observed at-issueness) and the observed projectivity.

Equations