AI for linguistics Lean checks

← Iconological Semantics (geometry) · raw TODO.md

TODO / extraction: geometric part of Schlenker & Lamberton, "Iconological Semantics" (L&P 2024)

Page numbers are the journal-manuscript page numbers printed at the foot of each page in source/Iconological-Semantics.pdf (txt line numbers in brackets refer to source/Iconological-Semantics.txt).

A. Definitions, formulas and claims to formalize

#ItemLocationLean
1Signer frame r*: 3 orthogonal axes, right-handed (x right, y front, z up), origin at center of signing space; signer's chest at (0,-1,0)ยง7.2, pp. 31-32 (83) [l. 1651-1665], (84c) p. 33signerFrame
2Same coordinate system "from the addressee's position (0,1,0), x toward the addressee's left, y toward their back, z up"p. 32 [l. 1665-1668]addressee_paper_frame_eq_signer, addressee_natural_frame
3Viewpoint pi determines frame r(pi), spatial scale s(pi) (>0), and temporal scale t(pi)p. 32, (84b) p. 33Viewpoint
4Classifiers and objects come with a center and an orientation = right-handed orthonormal triplep. 32, (84a)Pose, Pose.Valid, rightHanded_isRot
5center(d,r) = triple of reals; orientation(d,r) = <u,v,w> coordinates of the 3 vectors(84a)(i),(ii), p. 32-33center, orientation
6fn 45: orientation better defined as triple of anglesp. 33 fn 45not formalized (rotation matrices used; equivalent parametrization)
7(84d) lexical content word'_{t,w}p. 33parameter lex
8(85) proj(d,pi,t,w)=WORD iff (i) word'_{t,w}(d)=1 and (ii) a. center(d,r(pi)) = s(pi).center(WORD,r*), b. orientation(d,r(pi)) = orientation(WORD,r*)p. 33projStatic
9Example (86)-(89): Dalai Lama (0,0,0), Obama (50,0,0); orientations Obama <(0,1,0),(-1,0,0),(0,0,1)>, DL <(0,-1,0),(1,0,0),(0,0,1)>; scale 1/50; Obama classifier at (1,0,0); same orientations for the classifierspp. 33-35obama, clObama, example_*
10fn 47: viewer at (0,-10,0) (signer-like) or (0,10,0) (addressee-like)p. 33 fn 47covered by item 2 / signer_addressee_equivalence
11Claim: (85)(i) makes the lexical condition boxed in (53) redundantp. 35 [l. 1806-1810], fn 49lexical_condition_redundant (two-valued reading)
12(90) dynamic projection: (i) word'_{t,w}(d)=1 and (ii) for each d' <= d, proj(d,pi,t+t(pi)d',w) = word-cl(d'); dynamic classifier = function [0,d] -> static classifierspp. 35-36projDyn
13Flight example: 8 h shown as 2 s gives t(pi)=14,400p. 35example : 8*60*60/2 = 14400
14(91): classifier moves 1 s, scaling factor 5, object moves for 5 s mirroring the classifierp. 36example_dynamic
15fn 64 (Chemla p.c.): objects and classifiers are both points+frames; classifier true of object iff there is a geometric transformation (translations, rotations, scalings) from one to the otherp. 49 fn 64Sim, projSim, projStatic_iff
16App. I-E (126)-(128): loci; (127)=(85) copied; (128)(i) lexical = entity; center of locus = pointed part (head for person); orientation trivialized (128)(ii)bpp. 48-49projLocus, projLocus_iff_exists_orientation
17(129) numeric locus example: locus 30 cm above center, s=3, r(s(pi)) at 1.20 m => head at 2.10 mp. 49example_locus
18Remark p. 31: signer vs addressee viewpoint: scaling/marking can be done the same wayp. 31 [l. 1638-1645]signer_addressee_equivalence
19Rule (53)/(52): [[P_pi]](x) = 1 iff [[P]](x)=1 and proj(x,s(pi),t,w)=Ppp. 21-22absorbed in lexical_condition_redundant

B. Issues spotted in the original (see RESULTS.md for status)

  1. Scale direction contradicts the worked example. (85)(ii)a says center(d, r(pi)) = s(pi) . center(WORD, r*), i.e. s multiplies classifier coordinates to get object coordinates. The example (p. 34) takes s = 1/50 with Obama at 50 and the classifier at 1: that satisfies center(WORD) = s . center(d), the opposite direction. With (85) as written s must be 50. (The temporal scale in (90)/(91), 5 and 14,400, does go in the (85) direction, so (85) and (90) are mutually consistent and the example is the odd one out.) Lean: example_obama_s50, example_obama_paper_scale_fails.
  2. r* and r(pi) swapped in the prose of the example (p. 34): "the frame of reference notated as r* in (85)" is used for the scene's frame (that is r(pi)), and "the signer's frame of reference (notated as r(pi) in (85))" (that is r*).
  3. Orthonormality/handedness is only in prose. (84a)(ii) says "right-handed triple of orthogonal vectors of unit length" but nothing in (85) uses this; (85) is well defined and a fortiori satisfiable for arbitrary triples. Consequences: (a) the reconstructed characterization "exists a rotation carrying classifier to object" needs it (no_sim_to_mirror_pose, no_sim_to_nonunit_pose); (b) a left-handed object can never project on a right-handed classifier: mirror images are not handled (the "mirror-image version" of the Obama picture in fn 43 is only about the figure).
  4. Which vector is the "front"? The triple <u,v,w> has no stated meaning (front/side/up); the example is consistent with u being "front"-ish but nothing in (84) fixes it, and the classifier's own orientation convention is left to the lexicon.
  5. r(pi) and r* are unrelated a priori, and r(pi) is free (any frame): existential quantification over pi makes (85) trivially satisfiable for valid poses (exists_sim_of_valid). The constraint only bites because one viewpoint pi is shared by all classifiers of a scene (shared_viewpoint_distance, shared_viewpoint_relative_orientation). Same for fn 64: read as a plain existential over transformations it is vacuous.
  6. No time/world argument in center/orientation. (84a) center(d,r), orientation(d,r) have no t,w parameters although proj(d,pi,t,w) is evaluated at t,w and (90) requires the object's pose at times t+t(pi)d'. Also center(WORD,r*) of a dynamic classifier depends on d'. (Formalized by making obj, cl functions of time.)
  7. proj is a relation, written as a function. "proj(d,pi,t,w) = WORD" only makes sense as a relation: two classifier tokens with the same pose (or same word in different loci, cf. plane-cl_i, p. 22) would make it multi-valued. Argument order also differs: proj(d,pi,t,w) in (85) vs proj(pi,t,w,d) in (90).
  8. Notation clashes in (90). d = the object in (85) but the duration in (90) (and (90) header uses d as object argument while (ii) uses d' <= d as a time); t is the evaluation time, t(pi) the temporal scale, and word-cl_t (subscript t) marks dynamic classifiers; word'_{t,w} is again t. The range "for each d' <= d" omits d' >= 0. Fixed in Lean: dur, ts, 0 <= d' <= dur.
  9. (90)(i) is redundant (take d' = 0 in (ii), since (ii) re-imposes (85)(i) at t+t(pi).0 = t): projDyn_i_redundant. Conversely (85)(i) is evaluated at time t+t(pi)d' for each d', not only at t; harmless but the "lexical" condition thus must hold throughout (e.g. a sitting person must remain sitting while moving).
  10. Redundancy claim (p. 35, fn 49) is true only in the two-valued reading: (53) also handles the presupposition failure case [[P]](x)=#, which (85) (a condition on proj) does not (fn 49 second remark says similar for assignments).
  11. Uniform scale only; centers only scaled about the origin of r*. Fine given a similarity, but note that the formulation implicitly puts r*'s origin and r(pi)'s origin in correspondence; the elegant version makes the translation explicit (Viewpoint.toSim).
  12. Signer/addressee remark. The paper says the frame from the addressee's position (x = addressee's left, y = addressee's back, z up) is "the very same coordinate system". True: the axes coincide (addressee_paper_frame_eq_signer). The addressee's natural (right, front, up) axes are a 180 degree rotation about z of r* (addressee_natural_frame). Using them requires changing r* and r(pi) together (projStatic_rot); changing only one flips the verdict (example_one_sided_change_fails).
  13. fn 45's "triple of angles" is not a complete invariant (Euler angles have gimbal-lock/non-uniqueness); rotation matrices (or unit quaternions) are the clean choice.