ASL quantifier signs

This file records the quantificational signs of American Sign Language attested with locus and height modification in [DG22], under their ASL Signbank ID glosses, as the carrier Sign. A sign projects to a Quantifier record and denotes the readings the literature makes available for its gloss: FS(ALL) is the fingerspelled universal, ALL-b its two-handed form, NONEsym the symmetrical negative quantifier, and the numerals ONE and TWO carry both the at-least and the exactly reading. Which signs carry a height-marked locus themselves and which take a following IX-arc is a matter of their phonological form and is classified in the study, not here.

References

• K. Davidson and D. Gagne, "More is up" for domain restriction in ASL (2022)

inductive ASL.Determiners.Sign : Type

The quantifier signs attested in the paper.

• fsAll : Sign
• allB : Sign
• noneSym : Sign
• someone : Sign
• something : Sign
• one : Sign
• two : Sign
• many : Sign
• few : Sign
• each : Sign
• most : Sign

@[instance_reducible]

instance ASL.Determiners.instDecidableEqSign : DecidableEq Sign

Equations

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

@[instance_reducible]

instance ASL.Determiners.instReprSign : Repr Sign

Equations

• ASL.Determiners.instReprSign = { reprPrec := ASL.Determiners.instReprSign.repr }

def ASL.Determiners.instReprSign.repr : Sign → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• ASL.Determiners.instReprSign.repr ASL.Determiners.Sign.allB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ASL.Determiners.Sign.allB")).group prec✝
• ASL.Determiners.instReprSign.repr ASL.Determiners.Sign.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ASL.Determiners.Sign.one")).group prec✝
• ASL.Determiners.instReprSign.repr ASL.Determiners.Sign.two prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ASL.Determiners.Sign.two")).group prec✝
• ASL.Determiners.instReprSign.repr ASL.Determiners.Sign.many prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ASL.Determiners.Sign.many")).group prec✝
• ASL.Determiners.instReprSign.repr ASL.Determiners.Sign.few prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ASL.Determiners.Sign.few")).group prec✝
• ASL.Determiners.instReprSign.repr ASL.Determiners.Sign.each prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ASL.Determiners.Sign.each")).group prec✝
• ASL.Determiners.instReprSign.repr ASL.Determiners.Sign.most prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ASL.Determiners.Sign.most")).group prec✝

@[instance_reducible]

instance ASL.Determiners.instFintypeSign : Fintype Sign

Equations

• ASL.Determiners.instFintypeSign = { elems := { val := ↑ASL.Determiners.Sign.enumList, nodup := ASL.Determiners.Sign.enumList_nodup }, complete := ASL.Determiners.instFintypeSign._proof_1 }

def ASL.Determiners.Sign.form : Sign → String

The ASL Signbank ID gloss.

Equations

• ASL.Determiners.Sign.fsAll.form = "FS(ALL)"
• ASL.Determiners.Sign.allB.form = "ALL-b"
• ASL.Determiners.Sign.noneSym.form = "NONEsym"
• ASL.Determiners.Sign.someone.form = "SOMEONE"
• ASL.Determiners.Sign.something.form = "SOMETHING"
• ASL.Determiners.Sign.one.form = "ONE"
• ASL.Determiners.Sign.two.form = "TWO"
• ASL.Determiners.Sign.many.form = "MANY"
• ASL.Determiners.Sign.few.form = "FEW"
• ASL.Determiners.Sign.each.form = "EACH"
• ASL.Determiners.Sign.most.form = "MOST"

def ASL.Determiners.Sign.numberRestriction : Sign → Option Number

The grammatical number a sign selects.

Equations

• ASL.Determiners.Sign.fsAll.numberRestriction = some Number.plural
• ASL.Determiners.Sign.allB.numberRestriction = some Number.plural
• ASL.Determiners.Sign.two.numberRestriction = some Number.plural
• ASL.Determiners.Sign.many.numberRestriction = some Number.plural
• ASL.Determiners.Sign.few.numberRestriction = some Number.plural
• ASL.Determiners.Sign.most.numberRestriction = some Number.plural
• ASL.Determiners.Sign.someone.numberRestriction = some Number.singular
• ASL.Determiners.Sign.something.numberRestriction = some Number.singular
• ASL.Determiners.Sign.one.numberRestriction = some Number.singular
• ASL.Determiners.Sign.each.numberRestriction = some Number.singular
• ASL.Determiners.Sign.noneSym.numberRestriction = none

def ASL.Determiners.Sign.toQuantifier (s : Sign) : Quantifier

The sign as a determiner record.

Equations

• s.toQuantifier = { form := s.form, numberRestriction := s.numberRestriction }

def ASL.Determiners.Sign.toList : List Sign

All the signs.

Equations

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

@[instance_reducible]

noncomputable instance ASL.Determiners.Sign.instDenotesSetFamily : Semantics.Denotes Sign (Set Quantifier.GQ.Family)

The readings available for a sign, those of its gloss: the universals and EACH read as every, NONEsym as no, the existentials as Quantifier.GQ.some, FEW as few, MOST as most, and the numerals as atLeast or exactly; MANY has no reading, its standard being contextual.

Equations

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