PropertyDomain — Perceptual/Cognitive Channels for Adjective Dimensions

[GRFM26] [WH17]

A taxonomy of perceptual and cognitive channels a gradable dimension belongs to. color, material, and orientation are features known to guide visual search ([WH17]); [GRFM26] manipulates their perceptual discriminability and finds colour resists reduction to discriminability alone. These channels, together with size, carry the noise parameters used by the RSA reference model; the remaining domains are inventoried for typological completeness.

PropertyDomain is the codomain of Semantics.Gradability.Dimension.domain; the bridge to noise parameters (Features.PropertyDomain.noiseDiscrimination) lives in Pragmatics/RSA/Channel.lean.

inductive Features.PropertyDomain : Type

Broad perceptual/cognitive domain that a gradable dimension belongs to. color, size, material, and orientation carry noise parameters in RSA.Noise (via noiseDiscrimination); the rest are classified but not parameterised.

• color : PropertyDomain
• size : PropertyDomain
• material : PropertyDomain
• orientation : PropertyDomain
• sensory : PropertyDomain
• evaluative : PropertyDomain
• psychological : PropertyDomain
• state : PropertyDomain

@[implicit_reducible]

instance Features.instReprPropertyDomain : Repr PropertyDomain

Equations

• Features.instReprPropertyDomain = { reprPrec := Features.instReprPropertyDomain.repr }

def Features.instReprPropertyDomain.repr : PropertyDomain → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instDecidableEqPropertyDomain : DecidableEq PropertyDomain

Equations

• Features.instDecidableEqPropertyDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instInhabitedPropertyDomain : Inhabited PropertyDomain

Equations

• Features.instInhabitedPropertyDomain = { default := Features.instInhabitedPropertyDomain.default }