Image Schema Logic (ISL) is a formalism capable of expressing the spatio-temporal properties of image schemas. Its temporal component relies on linear temporal logic (LTL), which is not adequate for measuring and repeating time intervals, a fundamental aspect of rhythm. In this paper, we propose an extension of ISL which can express recurring time intervals of arbitrary length. We showcase its applicability by representing the moonwalk. Our research lays the groundwork for formal dance representation by emphasising the fundamental movement patterns of the moonwalk.
Image schemas are recurring structures of cognitive processes which describe the basic patterns for understanding the surrounding world, and reasoning about it. Understanding and representing these schemas is fundamental for the deep development of artificial intelligence. In particular, the field of knowledge representation can gain insights from the study of image schemas.
The study of image schemas starts from basic primitive concepts (intrinsic notions that are
universally grasped) which can then be combined into more complex events and concepts. One
primitive concept that has received little attention from the formal study of image schemas is,
surprisingly, that of rhythm. It has been argued and validated empirically, that human beings
and other animal species have an internal perception and representation of time [
One common manifestation of rhythm arises in the form of dance. Basic dance moves are, indeed, perfect examples of image schemas, which require spatio-temporal reasoning augmented with sensorimotor experiences by the dancer. The temporal dimension keeps track of the rhythm, often—but not always—aided through the perception of music or acoustic cues, while the spatial dimension reasons about distance, movements, and trajectories, using visual information about potential obstacles and limits. Complex dances are combinations of simple steps.
Image schema logic (ISL) [
In this paper, we aim to fill this gap by proposing a new temporal logic over linear time (LTL) which uses new temporal variables to account for the time intervals between “beats” in a rhythmic execution. In a nutshell, the semantics of our logic interprets each temporal variable with a specific real number that corresponds to the specific time manifestation of the rhythm in that interpretation. We also introduce a new constructor that requires that an event is observed exclusively at time points separated by those specific intervals. Thus, we can represent a kind of metronome that ticks at regular intervals and serves as a cue for rhythmic expressions.
Our language is expressive enough to represent the schemas of simple dance steps and other movements. As a prototypical example, we provide a simple description of the moonwalk, which is characterised by a clear backward movement, with continuous contact of the feet with the ground. The moonwalk’s predefined steps and relatively minimal emphasis on emotional and sociocultural dimensions typically associated with other dances make it an ideal starting point and a prime example that can be readily captured through formal representation. Needless to say, our language can express other properties as well. As we argue at the end, a full description of dance requires further extensions from a spatial point of view, but also a deeper understanding of social interaction, which may be beyond the study of image schemas per se.
Formally capturing how humans conceptualise complex psychosomatic events remains an
important multidisciplinary challenge [
This work attempts to capture and represent the dynamic interactions and interdependencies
between these dance components to gain a better understanding of the complex human
mindbody relationship. Formalisation and conceptualisation of complex psychosomatic events such
as dance can have broader implications for fields such as therapy [
Given the complexity of dance, it is important to consider an appropriate starting point, which is selecting a dance style that is relatively easier to formally represent using image schemas. Within this context, several factors should be taken into account, including distinctive movement patterns, a clear spatiotemporal relationship between the dancer’s feet and the ground, limited complexity, visual clarity and dance that can be considered as a well-known reference point for both researchers and dancers. The visual, temporal and spatial elements of the moonwalk can be readily captured and analysed as image schemas, allowing for a comprehensive understanding of its execution. It is a popular dance move that possesses characteristics which make it easier to represent compared to other dance styles. The movement pattern of the moonwalk primarily relies on a unique spatiotemporal relationship between the dancer’s body and the ground as the dancer appears to be moving forward while in actuality they are moving backwards [16]. To perform the moonwalk, the dancer starts in an upright position with feet close together. Next, the dancer shifts the weight to one foot while keeping the other foot slightly lifted of the ground. After that, the dancer starts sliding the lifted foot backwards, keeping it in contact with the floor as much as possible while performing smooth and controlled movements. The dancer then slightly lifts the heel of the sliding foot to allow the smooth gliding motion as they slide the foot backwards. At the same time, the supporting leg should be slightly bent to maintain balance and control. The dancer then repeats the step with the other foot after the sliding foot after the sliding foot reaches its maximum extension. During the foot movement, it is also important to coordinate the upper body by keeping it aligned with the hips and legs with subtle backwards leaning to enhance the illusion of a moonwalk [17]. Focusing on these key spatiotemporal relationships, image schemas can be used to efectively capture the basic essence of the moonwalk and formalise its representation.
Cognitive and sensorimotor processes are integral components of dance execution [18, 19]. These processes involve the interpretation and integration of sensory information (through spatial, temporal [20] and body perception [21]), motor planning and control [22] as well as the embodiment of emotional and sociocultural narratives [23].1 While performing a moonwalk, dancers need to accurately perceive their body position, alignment and movement in relation to the environment and maintain a sense of distance and direction while planning and controlling their movements in a synchronous and rhythmic manner. This integration of sensory and motor processes in dance execution relies on complex neurocognitive processes [20]. The dancer must shift their weight, slide one foot backwards while keeping it in contact with the floor, and coordinate their posture to enhance the illusion of walking forward. This 1While the physical execution of the moonwalk itself may be relatively simple, the dance is not inherently dictated by specific emotions and sociocultural dimensions. While these dimensions allow dancers to inject their creativity, individuality and personal meaning into the performance, this work is mainly interested in the basic skeletal notion of the dance and, therefore, these dimensions would not be considered further. requires precise control over muscle activation, coordination and planning in terms of following the steps. Temporal processing (i.e. perception and processing of time), in particular, play a crucial role in the mentioned movement coordination and rhythm maintenance during dance performances. Temporal perception is the ability of the brain to perceive the passage of time, allowing individuals to make temporal judgements, synchronise their actions, and perceive rhythmic patterns [24]. Recent neuroscientific studies shed light on the mechanisms underlying time perception. The brain possesses specialised neural circuits and structures involved in temporal processing, such as the basal ganglia, cerebellum, and supplementary motor area. These regions work together to encode, represent, and synchronize temporal information [25]. Although temporal and rhythmic perception are related concepts, there are some diferences between them as temporal perception relates to the broader understanding of time and the coordination of movements, while rhythm perception specifically focuses on the interpretation and expression of rhythmic patterns within the context of dance. However, in terms of neurological processing of both time and rhythm, the brain has evolved to handle both types of processing naturally. As the ability to perceive and process both time and rhythm has a basis in our neural architecture it might not require explicit representation by image schemas [26].
Image Schema Logic (ISL) [
While ISL is a very expressive language, capable of representing the main features of image schemas, some cognitive elements still remain out of its reach. In particular, LTL is quite limited in some features regarding time measurement. In its standard form, this logic can express properties that will occur eventually (at some point in the future) or within a specific timeframe. Yet, this fails to account for the subjective time measures that one encounters, for instance, in rhythm and dance. In these cases, the precise amount of time between “beats” is irrelevant, but it is important that the same time gap is persistent through a sequence of beats. The moonwalk, for instance, is not only about the movement of feet going backwards but must preserve a flow obtained by taking the same amount of time between steps. Without it, the movement will look unnatural. In Section 3 we introduce a variant of temporal logic which can express these properties and instantiate it with the moonwalk.
While in the context of image schemas, rhythm, and time, a potentially relevant schema is that
of circularity or movement in loops [
We propose an extension of LTL over the reals that is capable of expressing events that repeat at recurrent time intervals, but without fixing a priori the length of these intervals. Although the underlying semantics use the real numbers for the temporal evolution, the new constructor in part discretises the time measurement.
The logic LTL extends LTL with two new constructors B and ℓB which we call beat and limited beat, respectively, which express the repetition of events at uniform intervals. For brevity, we introduce only the version of LTL that can only speak about the future of events; yet its extension to the past is straightforward.
Formally, LTL formulas are built from a set of propositional variables, and a set of time variables through the grammar rule
::= | ¬ | ∧ | | B | ℓB where ∈ and ∈ . The semantics uses the dense line of non-negative real numbers R≥ 0 with the standard total order over its elements. Specifically, an interpretation is a pair I = (, ) where : → 2R≥ 0 is the propositional valuation, which maps each propositional variable to a subset of R≥ 0, and : → R≥ 0 is the interval specification . Intuitively, propositional valuation expresses at which moments in time each variable ∈ is true, while the interval specification states how long the time intervals between beats will be.
The satisfaction of an LTL formula at time ∈ R≥ 0 under the interpretation I is defined inductively by: • I, |= if ∈ (); • I, |= ¬ if I, ̸|= ; • I, |= ∧ if I, |= and I, |= ; • I, |= if there is < ∈ R≥ 0 such that (i) I, |= and (ii) for all < <
I, |= ; • I, |= B if for every ∈ R≥ 0 it holds that I, + |= if = · () for some ∈ N+; and • I, |= ℓB if there exists ∈ N+ such that (i) I, + · () |= for all 1 ≤ ≤ , ∈ N+ and (ii) I, + ̸|= for all other , 0 < < · () We are often interested in verifying whether I, 0 |= for some formula . In this case, we say that I is a model of .
Intuitively, the formula B describes a beat of a given (arbitrary but fixed) length () (given by the interval specification over the time variable ) where we will observe happen.2 2Note that the first beat happens when time () has passed, the second after a wait of time 2 () after the first, and so on.
One can understand this as the tick of a clock or as the base rhythm of a drum. In this case, the beat will be repeated forever. The formula ℓB has a bounded reach, expressing that the beat may stop or change after a finite (but, again, arbitrary) number of steps. The idea is to use these beats to enforce that events are observed with a certain regularity.
Importantly, the interpretation of the length of time represented by the time variable is ifxed once we decide on the interval specification. This allows us to speak about diferent events which all repeat within the same period. In addition, using more than one-time variable, we can have diferent beats interacting with each other. For example, considering the event of walking (or dancing), one expects each step to happen with temporal regularity, and yet it is impossible to specify its period beforehand: in some cases, one may walk faster than in others. Simultaneously, one may expect the walker to breathe regularly, but not necessarily with the same rhythm as they walk.
As mentioned, the new constructors discretise the timeline into beats, so it may seem as if our logic is just a characterisation of discrete time LTL. Yet, our language is stronger than classical LTL. Consider for instance the formula := B ∧ B′ ( ∧ ). The first conjunct of the formula expresses that is observed in () intervals. Let us use this () as a measure of a beat. By our semantics, ∧ will repeat every beats, for some arbitrary ∈ N+. In more detail, ∧ has to be observed in (′) intervals, but to observe ∧ we must necessarily observe , which is only available at each beat; i.e., (′) = · () for some ∈ N+. In words, the formula is satisfied if ∧ is observed in every beat, or every two beats, or every three beats, or . . . . This formula schema characterises a language that is not -regular [31], and hence not expressible in (discrete) LTL [32].
We use the two typical abbreviations F := ⊤ and G := ¬F¬ where ⊤ stands for any (first-order) tautology. Intuitively
F expresses that will hold at some point in the future, while G expresses that always in the future holds.
The basic description of a moonwalk is provided in Section 2.1. Here we formalise it using the variant of ISL that uses LTL as its temporal component.
Abstracting from the fine-grained movements of the diferent parts of the body, the moonwalk is characterised by backward steps where the front foot is moved backwards (relative to the perceiver) for a fixed amount of time (a “beat”), reaching a mirror position of the feet, and then immediately repeating the movement from the new position. This simple pattern is repeated an arbitrary number of times.
First, we need to specify the moments where the beat takes place; which is possible through the expression Bbeat. This means that at regular intervals beat holds (and nowhere else). The rest of the movement revolves around this event. At every beat, one foot should be in front and one behind the dancer. Considering two objects and standing for the left and right foot, this is expressed through the formula
︂( position := G beat ↔ ︀( ( (, Me) ∧ (Me, )) ∨ ( (, Me) ∧ (Me, )))︀ .
︂) Putting these ingredients together, we can now formalise the moonwalk with the formula
Bbeat ∧ ∀, : , , : .(︀ position ∧ G(Contact(, ) ∧ Contact(, )) ∧ (beat ∧ (, Me) → ( ⇝ ∧ |∘ )) ∧ (beat ∧ (, Me) → ( ⇝ ∧ |∘ )))︀ , where and represent the ground (both feet should keep contact with the ground at all times) and the back of the perceiver (the front foot should move towards the back, while the other one remains still), respectively.
One can obviously elaborate on this schema to provide a more precise description of the specific dance move by e.g., describing the rise of the heel or the movements of the hands and the upper body. Such specifications are beyond the scope of this paper, where the main elements for expressing dance moves, and in particular rhythm, are introduced.
In this work, we have considered an extension of the Image Schema Logic (ISL) which is capable of expressing regular occurrences of events, where the repetition period is not fixed a priori, but rather identified in the interpretation of a so-called temporal variable. Our motivation arises from the need to represent dance moves, which depend on a primitive concept of rhythm. Indeed, rhythm is a universal notion, with intercultural and interspecies manifestations [33]. Yet, usual temporal logics are incapable of representing it, as it refers to time regularity, which is independent of the specific amount of time taken. Dance is a movement manifestation and expression of rhythm. Of course, it is not only in dance but in many other activities and events, including simple actions like walking that rhythm manifests itself.
While our work provides a foundation for formal dance representation by focusing on the fundamental movement patterns of the moonwalk, incorporating emotions and sociocultural dimensions would provide a more thorough and complete overview of dance as a complex psychosomatic event. The moonwalk serves as a starting point since its representation through image schemas does not require consideration of emotions and social dimensions due to its clear and simple movement patterns. However, exploring how emotions and sociocultural dimensions may be represented would build upon this foundation and provide important insights into how they shape and influence the human mind-body relationship in dance and generate a more holistic understanding of dance as a complex psychosomatic phenomenon. Even at the level of image schemas, extending the spatial dimension to deal with abstract distances (steps have the same length) and trajectories (movement towards an object and beyond) will be useful for dealing with the properties of dance and movement.
Beyond the interest of dealing with image schemas, we plan to further study the expressivity and computational properties of LTL, in order to understand what other elements it can express, and provide clear guidelines for how it can be used.
This work was partially supported by the MUR for the Department of Excellence DISCo at the University of Milano-Bicocca and under the PRIN project PINPOINT Prot. 2020FNEB27, CUP H45E21000210001. search for designing and evaluating wearable human-computer interfaces, in: Proceedings of the 8th International Conference on Movement and Computing, 2022, pp. 1–9. [15] Q. Zhou, C. C. Chua, J. Knibbe, J. Goncalves, E. Velloso, Dance and choreography in hci: a two-decade retrospective, in: Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems, 2021, pp. 1–14. [16] M. Yim, New locomotion gaits, in: Proceedings of the 1994 IEEE International conference on Robotics and Automation, IEEE, 1994, pp. 2508–2514. [17] M. Pugh, America Dancing: from the Cakewalk to the Moonwalk, Yale University Press, 2015. [18] B. Bläsing, B. Calvo-Merino, E. S. Cross, C. Jola, J. Honisch, C. J. Stevens, Neurocognitive control in dance perception and performance, Acta psychologica 139 (2012) 300–308. [19] L. Okonski, Beneath the beauty of dance: A cognitive approach to kinesthetic intelligence, 2012. [20] A. M. Ladda, S. B. Wallwork, M. Lotze, Multimodal sensory-spatial integration and retrieval of trained motor patterns for body coordination in musicians and dancers, Frontiers in Psychology 11 (2020) 576120. [21] C. Jola, A. Davis, P. Haggard, Proprioceptive integration and body representation: insights into dancers’ expertise, Experimental brain research 213 (2011) 257–265. [22] G. Batson, Update on proprioception: considerations for dance education, Journal of
Dance Medicine & Science 13 (2009) 35–41. [23] J. L. Hanna, A nonverbal language for imagining and learning: Dance education in k–12 curriculum, Educational Researcher 37 (2008) 491–506. [24] J. Phillips-Silver, C. A. Aktipis, G. A. Bryant, The ecology of entrainment: Foundations of coordinated rhythmic movement, Music perception 28 (2010) 3–14. [25] S. A. Kotz, M. Schwartze, Diferential input of the supplementary motor area to a dedicated temporal processing network: functional and clinical implications, Frontiers in Integrative Neuroscience 5 (2011) 86. [26] P. Amos, Rhythm and timing in autism: Learning to dance, Frontiers in integrative neuroscience 7 (2013) 27. [27] M. M. Hedblom, Image Schemas and Concept Invention - Cognitive, Logical, and Linguistic Investigations, Cognitive Technologies, Springer, 2020. URL: https://doi.org/10.1007/ 978-3-030-47329-7. doi:10.1007/978-3-030-47329-7. [28] M. Reynolds, The complexity of temporal logic over the reals, Annals of Pure and Applied
Logic 161 (2010) 1063–1096. doi:https://doi.org/10.1016/j.apal.2010.01.002. [29] D. A. Randell, Z. Cui, A. G. Cohn, A spatial logic based on regions and connection, in: B. Nebel, C. Rich, W. R. Swartout (Eds.), Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR’92), Morgan Kaufmann, 1992, pp. 165–176. [30] N. V. de Weghe, A. G. Cohn, P. D. Maeyer, A qualitative representation of trajectory pairs, in: R. L. de Mántaras, L. Saitta (Eds.), Proceedings of the 16th European Conference on Artificial Intelligence, ECAI’2004, IOS Press, 2004, pp. 1103–1104. [31] W. Thomas, Automata on infinite objects, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier and MIT Press, 1990, pp. 133–191. URL: https://doi.org/10.1016/b978-0-444-88074-1.50009-3. doi:10.1016/ b978-0-444-88074-1.50009-3. [32] M. Y. Vardi, P. Wolper, Reasoning about infinite computations, Inf. Comput. 115 (1994) 1–37. URL: https://doi.org/10.1006/inco.1994.1092. doi:10.1006/inco.1994.1092. [33] A. Ravignani, Rhythm and synchrony in animal movement and communication, Current Zoology 65 (2018) 77–81. doi:10.1093/cz/zoy087.