ASL Classifier Predicates

@cite{schlenker-lamberton-2024} @cite{schlenker-lamberton-lamberton-2026}

Lexical entries for ASL classifier predicates used in the elicited paradigms of @cite{schlenker-lamberton-lamberton-2026}. Each classifier has a handshape that iconically represents a class of objects, and its position/movement in signing space is interpreted relative to a viewpoint.

Classifiers

Gloss	Handshape	Object class
TREE-cl	1-hand (upright index finger)	trees
POLE-cl	1-hand (upright index finger)	poles, posts
PERSON-cl	index finger (upright)	people
VEHICLE-cl	3-hand (thumb + index + middle)	vehicles, cars
WALL-cl	open hand (upright, flat)	walls, flat surfaces
RECTANGLE-cl	two-handed rectangle	rectangular objects
CORNER-cl	two-handed L-shape	corners

opaque Fragments.ASL.SigningSpace : Type

Abstract signing space. The position type for ASL classifier predicates. Concrete spatial geometry (Cartesian coordinates, scaling factors) is left for future extension.

inductive Fragments.ASL.Entity : Type

An entity type for ASL classifier constructions.

• ann : Entity
• tree : Entity
• pole : Entity
• house : Entity
• vehicle : Entity
• wall : Entity
• corner : Entity
• rectangle : Entity

@[implicit_reducible]

instance Fragments.ASL.instDecidableEqEntity : DecidableEq Entity

Equations

• Fragments.ASL.instDecidableEqEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.ASL.instReprEntity : Repr Entity

Equations

• Fragments.ASL.instReprEntity = { reprPrec := Fragments.ASL.instReprEntity.repr }

def Fragments.ASL.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Fragments.ASL.instReprEntity.repr Fragments.ASL.Entity.ann prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.ASL.Entity.ann")).group prec✝
• Fragments.ASL.instReprEntity.repr Fragments.ASL.Entity.tree prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.ASL.Entity.tree")).group prec✝
• Fragments.ASL.instReprEntity.repr Fragments.ASL.Entity.pole prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.ASL.Entity.pole")).group prec✝
• Fragments.ASL.instReprEntity.repr Fragments.ASL.Entity.wall prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.ASL.Entity.wall")).group prec✝

def Fragments.ASL.isTree : Entity → Prop

Logical predicate: is the entity a tree?

Equations

• Fragments.ASL.isTree Fragments.ASL.Entity.tree = True
• Fragments.ASL.isTree x✝ = False

@[implicit_reducible]

instance Fragments.ASL.instDecidablePredEntityIsTree : DecidablePred isTree

Equations

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

def Fragments.ASL.isPole : Entity → Prop

Logical predicate: is the entity a pole?

Equations

• Fragments.ASL.isPole Fragments.ASL.Entity.pole = True
• Fragments.ASL.isPole x✝ = False

@[implicit_reducible]

instance Fragments.ASL.instDecidablePredEntityIsPole : DecidablePred isPole

Equations

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

def Fragments.ASL.isPerson : Entity → Prop

Logical predicate: is the entity a person?

Equations

• Fragments.ASL.isPerson Fragments.ASL.Entity.ann = True
• Fragments.ASL.isPerson x✝ = False

@[implicit_reducible]

instance Fragments.ASL.instDecidablePredEntityIsPerson : DecidablePred isPerson

Equations

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

def Fragments.ASL.isVehicle : Entity → Prop

Logical predicate: is the entity a vehicle?

Equations

• Fragments.ASL.isVehicle Fragments.ASL.Entity.vehicle = True
• Fragments.ASL.isVehicle x✝ = False

@[implicit_reducible]

instance Fragments.ASL.instDecidablePredEntityIsVehicle : DecidablePred isVehicle

Equations

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

def Fragments.ASL.isWall : Entity → Prop

Logical predicate: is the entity a wall or flat surface?

Equations

• Fragments.ASL.isWall Fragments.ASL.Entity.wall = True
• Fragments.ASL.isWall x✝ = False

@[implicit_reducible]

instance Fragments.ASL.instDecidablePredEntityIsWall : DecidablePred isWall

Equations

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

def Fragments.ASL.isRectangle : Entity → Prop

Logical predicate: is the entity a rectangular object?

Equations

• Fragments.ASL.isRectangle Fragments.ASL.Entity.rectangle = True
• Fragments.ASL.isRectangle x✝ = False

@[implicit_reducible]

instance Fragments.ASL.instDecidablePredEntityIsRectangle : DecidablePred isRectangle

Equations

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

def Fragments.ASL.isCorner : Entity → Prop

Logical predicate: is the entity a corner?

Equations

• Fragments.ASL.isCorner Fragments.ASL.Entity.corner = True
• Fragments.ASL.isCorner x✝ = False

@[implicit_reducible]

instance Fragments.ASL.instDecidablePredEntityIsCorner : DecidablePred isCorner

Equations

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

def Fragments.ASL.treeCl (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : Semantics.Iconic.ClassifierPred Entity SigningSpace

TREE-cl: 1-handshape classifier for trees. Viewpoint variable π₀ (free by default).

Equations

• Fragments.ASL.treeCl proj = { logical := Fragments.ASL.isTree, projects := proj, viewpointVar := Semantics.Iconic.ViewpointVar.free 0, label := "TREE-cl" }

def Fragments.ASL.poleCl (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : Semantics.Iconic.ClassifierPred Entity SigningSpace

POLE-cl: 1-handshape classifier for poles. Viewpoint variable π₀ (free by default).

Equations

• Fragments.ASL.poleCl proj = { logical := Fragments.ASL.isPole, projects := proj, viewpointVar := Semantics.Iconic.ViewpointVar.free 0, label := "POLE-cl" }

def Fragments.ASL.personCl (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : Semantics.Iconic.ClassifierPred Entity SigningSpace

PERSON-cl: index finger classifier for people. Viewpoint variable π₀ (free by default).

Equations

• Fragments.ASL.personCl proj = { logical := Fragments.ASL.isPerson, projects := proj, viewpointVar := Semantics.Iconic.ViewpointVar.free 0, label := "PERSON-cl" }

def Fragments.ASL.vehicleCl (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : Semantics.Iconic.ClassifierPred Entity SigningSpace

VEHICLE-cl: 3-handshape classifier for vehicles. Viewpoint variable π₀ (free by default).

Equations

• Fragments.ASL.vehicleCl proj = { logical := Fragments.ASL.isVehicle, projects := proj, viewpointVar := Semantics.Iconic.ViewpointVar.free 0, label := "VEHICLE-cl" }

def Fragments.ASL.wallCl (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : Semantics.Iconic.ClassifierPred Entity SigningSpace

WALL-cl: open hand classifier for walls / flat surfaces.

Equations

• Fragments.ASL.wallCl proj = { logical := Fragments.ASL.isWall, projects := proj, viewpointVar := Semantics.Iconic.ViewpointVar.free 0, label := "WALL-cl" }

def Fragments.ASL.rectangleCl (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : Semantics.Iconic.ClassifierPred Entity SigningSpace

RECTANGLE-cl: two-handed classifier for rectangular objects.

Equations

• Fragments.ASL.rectangleCl proj = { logical := Fragments.ASL.isRectangle, projects := proj, viewpointVar := Semantics.Iconic.ViewpointVar.free 0, label := "RECTANGLE-cl" }

def Fragments.ASL.cornerCl (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : Semantics.Iconic.ClassifierPred Entity SigningSpace

CORNER-cl: two-handed L-shape classifier for corners.

Equations

• Fragments.ASL.cornerCl proj = { logical := Fragments.ASL.isCorner, projects := proj, viewpointVar := Semantics.Iconic.ViewpointVar.free 0, label := "CORNER-cl" }

theorem Fragments.ASL.treeCl_free (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : (treeCl proj).viewpointVar = Semantics.Iconic.ViewpointVar.free 0

All default classifiers use free viewpoint variables.

theorem Fragments.ASL.poleCl_free (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : (poleCl proj).viewpointVar = Semantics.Iconic.ViewpointVar.free 0

theorem Fragments.ASL.personCl_free (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : (personCl proj).viewpointVar = Semantics.Iconic.ViewpointVar.free 0

theorem Fragments.ASL.vehicleCl_free (proj : Entity → Semantics.Iconic.StaticViewpoint SigningSpace → Bool) : (vehicleCl proj).viewpointVar = Semantics.Iconic.ViewpointVar.free 0