text:
Elizabeth De Freitas
email: l.de-freitas@mmu.ac.uk

Nathalie Sinclair

Mathematical gestures: Multitouch technology and the indexical trace

Keywords: Technology, multitouch, number and operations, gesture

This paper is about the threshold between gesture and touch in mathematical activity, focusing on the role of multitouch technology. Drawing on the work of gesture theorist Jürgen Streek, we propose and discuss the notion of the tangible gesture, in the context of mathematical explorations of young children with a novel, multitouch iPad environment called TouchCounts designed to promote counting on and with the fingers.

Introduction

With the advent of multitouch technologies, gestures have become an essential feature of user interface. Touch technologies break with previous computer-based norms, where the hand's actions were indirectly related to changes on the screen through mouse and keyboard manipulation. Touch technology invokes earlier drawing technologies in which the hand's actions had a more direct relation with a given surface. The digital nature of contemporary surfaces, however, significantly alters the relation between touching and meaning-making.

In this paper, we draw attention to the distinctive gestures new media elicit and produce and the way these new manual activities are changing the way we perform mathematics. We also interrogate the taken-for-granted distinction between the touchscreen gestures common in the technology world and the in-the-air gestures that have been the focus of study in mathematics education research. At first blush, they may seem quite distinct-albeit having the same word-but we follow [START_REF] Streeck | Gesturecraft: The manu-facture of meaning[END_REF] in seeing them as being on a continuum, a perspective that enables us to better appreciate the role that touchscreen gestures might have in mathematics learning.

In the context of mathematics education research, many studies have focused on student and teacher use of gesture in classrooms, but this work tends to code and sort gestures insofar as they are representations of thinking. These studies tend to divorce the motoric hand from the feeling swipes and swishes of fingers on screens. Material semiotic approaches to the study of interaction, on the other hand, consider gesture less as representations and more in terms of the material effects they achieve [START_REF] Roth | Gestures: Their role in teaching and learning[END_REF][START_REF] Radford | The seen, the spoken and the written: A semiotic approach to the problem of objectification of mathematical knowledge[END_REF][START_REF] Nemirovsky | Gesture and imagination: On the constitution and uses of phantasms[END_REF]. Our goal in this paper is to unpack the implications for understanding mathematics learning in relation to new media. In order to illustrate how these new media gestures operate as expressions of numeracy, we draw on research involving a novel multitouch App in which fingers and gestures are used to count [START_REF] Jackiw | TouchCounts. Application for the iPad[END_REF].

Gesture as movement

The predominant line of research in gesture studies focuses on movements of the body (especially the hand) and their interactions (i.e. correlations) with speech in communication (Kendon, 2000[START_REF] Kendon | Gesture: Visible action as utterance Cambridge[END_REF][START_REF] Kita | Pointing: Where Language, Culture, and Cognition Meet[END_REF][START_REF] Mcneill | Hand and mind: What gestures reveal about thought[END_REF][START_REF] Mcneill | Gesture and thought[END_REF] (icon, metaphoric, deictic and beat) so as to distinguish different relations between gesture and speech. McNeill has drawn on [START_REF] Peirce | Elements of Logic[END_REF] semiotics in which signs (icons, symbols, and indices) differ in terms of the nature of the relationships between the signifying sign and the signified. These categories have been used extensively in mathematics education research.

Research that codes gesture only in terms of linguistic potential tends to overlook the physicality of the hand movement, except insofar as such movement contributes to or obscures linguistic meaning [START_REF] Rossini | Reinterpreting gesture as language: Language in action[END_REF]. As [START_REF] Streeck | Gesturecraft: The manu-facture of meaning[END_REF] indicates, "it is common to treat gesture as a medium of expression, which meets both informational and pragmatic or social-interactional needs, but whose "manuality" is accidental and irrelevant" (p. 39). [START_REF] Streeck | Gesturecraft: The manu-facture of meaning[END_REF] defines gesture:

… not as a code or symbolic system or (part of) language, but as a constantly evolving set of largely improvised, heterogeneous, partly conventional, partly idiosyncratic, and partly culturespecific, partly universal practices of using the hands to produce situated understandings. (p.5) Thus he studies gesture for how it is "communicative action of the hands" with emphasis on the term action (p.4). This focus on action allows Streeck to study gesture for how it couples with and intervenes in the material world in non-representational ways. Researchers often distinguish between hand movements in the air and hand movements that make graphic marks, where the former is deemed a gesture and the latter an act of inscription. However, such distinctions become fuzzy when we study the movement of the hand across and through media, where 'media' can be more or less receptive of trace or mark. In other words, all hand movements traverse and incorporate media. We see a trace in certain media, and not in others, but since the logic of new media is to break with current conventions of perception, this distinction is provisional. New media allow for new kinds of traces. This insight allows for new ways of studying numeracy and multitouch technologies. In the next section, we discuss a case study of children working with such technologies, showing how this material encounter entails a very different concept of number precisely because of the indexical aspect of gesture.

The question of trace and inscription returns us to how the indexical is different from the iconic. The contiguity aspect of indexicality (the smoke is materially caused and coupled with the fire) is aligned with touch and the way our body connects with another through touch. This approach to gesture supports the systems approach to bodies by which bodies become coupled with the environment they inhabit [START_REF] Maturana | The tree of knowledge: The biological roots of human understanding[END_REF]. Streeck studies gestures as part of a nested scaling approach to this system, beginning in the world that the "hand knows best", and then examining how gestures operate at greater distance or remove from that world (p. 58). The touch or haptic factor of hand movement is precisely how the fragile interface of inscription or trace is currently produced. Again, we emphasize that this production of a trace is contingent on current configurations of sensory perception and material media.

Most of the hand's features (digits, degrees of freedom of movement, fatty palms, flexure lines, papillary ridges) evolved to facilitate grasping (prehension), and thus the hand "became a 'compromise organ'" in serving multiple purposes [START_REF] Streeck | Gesturecraft: The manu-facture of meaning[END_REF]. Prehensile "postures" are formed as the hand reaches its target (in our case this will be a screen), during which a preconscious calibration of speed and collective force determines the particular movement of the digits, hands and arm. As the hand moves towards the target, there is a strong reliance on peripheral vision rather than vision directed at the target (Streeck, 2009, p.47). The speed of the gesture reduces as the hand reaches its target. But the moment of contact entails the forming of a new assemblage, when the entire body of the gesturer links up with that which it touches. Thus, we are focusing on how gesture is a hand action that does more than identify or code particular aspects of an object.

The video data discussed below is part of a larger project exploring the power of touchscreen technologies in teaching and learning mathematics in early childhood. Several research studies have already been carried out concerning the way that children learn various concepts using TouchCounts, including ordinality [START_REF] Sinclair | A trillion is after one hundred': early number and the development of symbolic awareness[END_REF], place value [START_REF] Coles | Re-thinking Place Value: From Metaphor to Metonym[END_REF] and finger gnosis [START_REF] Sinclair | Mathematics using multiple sense: Developing finger gnosis with three-and four-year-olds in an era of multi-touch technologies[END_REF]. The focus of this paper is less on the learning process using TouchCounts than on the various and distinctive forms of hand actions that are involved in creating and manipulating number in this environment.

What is distinctive about the index is that it is a sign that is materially linked or coupled to "its object". According to [START_REF] Peirce | Elements of Logic[END_REF], an index "refers to its object not so much because of any similarity or analogy with it, (…) as because it is in dynamical (including spatial) connection both with the individual object, on the one hand, and with the senses or memory of the person for whom it serves as a sign, on the other" (2.305). For instance, the chalk drawing of a parallelogram on a blackboard is often considered to be an iconic reference to a Platonic conception of parallelogram, but it is (also) an indexical sign that refers to the prior movement of the chalk. This latter indexical dimension is usually not emphasized in the semiotic study of mathematical meaning making, since we tend to focus on the completed trace and dislocate it from the labour that produced it. This focus on the completed sign neglects how the activity of the body and various other material encounters factor in mathematical activity.

TouchCounts: A multitouch early number App

In this paper, we discuss an application that author Sinclair has been involved in creating in which the digital gesture plays an even more central role in the mathematical activity. TouchCounts [START_REF] Jackiw | TouchCounts. Application for the iPad[END_REF]) is an application that permits young learners to coordinate simultaneously various forms of number: number names like 'three', number of taps on the screen, number of discs on the screen and number symbols like 3. It enacts a multimodal correspondence between finger touching, numeral seeing and number-word hearing (a one-to-one-to-one correspondence of touch, sight and sound). The App has two worlds: the Enumerating and the Operating worlds. In this paper, we focus on the Enumerating world, which is the one that children usually first experience.

In the Enumerating World, the screen starts almost blank, except for a horizontal bar called a shelf. In this world, a learner taps her fingers on the screen to summon numbered discs. The first tap produces a new yellow disc on which the numeral "1" appears. Subsequent taps produce sequentially higher numbered discs. As each tap summons a new numbered disc, TouchCounts audibly speaks the name of its numeral ("one," "two"). As long as the user's finger remains on the glass, it holds the numbered disc, but as soon as she "lets go" (by lifting her finger) virtual gravity makes the number object fall to and "off" the bottom of the screen. If the user releases her numbered disc above the shelf, or "flicks" it above the shelf on release, it falls only to the shelf, and comes to rest there, visibly and permanently on screen, rather than vanishing out of sight "below" (see https://www.youtube.com/watch?v=7xD-pqnsce0). Since each time a finger is placed on the screen, a new numbered object is created, one cannot "catch" or reposition an existing numbered disc by retapping it. We note that, at least initially, the eye plays a prominent role in directing the finger above or below the shelf, but that if one does not care where the disc alights, the tapping of the finger needs little visual direction.

If we take the finger tap as a gesture involving the placement of a finger on the screen, and the subsequent production of an event featuring visual, mobile and aural aspects, then we might say that the gesture is iconic in its relation to the production of unitary quantities, or perhaps even metaphorical for the children for whom such unitary quantities are still "abstract". But what seems much more pertinent for the children as they engage with this application is the indexical nature of the gesture. The tap both points to the screen, designating one place of contact with it, but also creates a new numbered disc under the soft skin of the finger-pad, a disc which often falls with gravity-like weight. In addition, each tap produces a simultaneous sound. The children can also tap the Reset button, which makes all the numbered discs disappear and resets the count to 1.

While TouchCounts was designed to support the development of one-to-one correspondence between number and hand movement, by drawing on the tangible dimension of counting, its use by young children has prompted us to examine both the particular ways in which they use their hands and the implications of their hand actions on the meanings they make around counting, in particular the concepts of ordinality and cardinality (see [START_REF] Sinclair | Mathematics using multiple sense: Developing finger gnosis with three-and four-year-olds in an era of multi-touch technologies[END_REF].

A case study

This case study is drawn form a broader research project that was conducted in daycare and primary school settings over the course of three years. In the excerpt we present, co-author Sinclair was engaged in a clinical interview with a five-year-old kindergarten child named Katy, who is interacting with TouchCounts for the first time. (Indeed, it was the first time she was using a touchscreen tablet.) The interview occurs in June and therefore close to the end of the school year. We have chosen the excerpt because it illustrates a range of gestures that have been observed over the course of the research study, while also showing hand motions that have not been explicitly taught. In this case study, the hand actually operates very close to the surface of a screen: pointing to objects on the screen by tapping them; sliding objects along on the screen so as to leave visual and aural traces of the finger's path; pinching objects together in order to make new ones.

The room is quiet. Without prompting, Katy's hand approaches the screen, and her finger touches the top of it and slides down to the bottom. A yellow disc appears under her finger with the numeral '1' on it and the sound 'one' is made. The index finger moves back to the top of the screen, slowly swimming downwards. A chorus of 'two' comes both from her mouth and the iPad. This happens repeatedly, although sometimes only the iPad can be heard announcing the new numbered disc while Katy's lips move in synchrony (Figure 1a). The appearance of '10' on the tenth yellow disc attracts attention, perhaps because of its double digits, and Katy bends over to look closely. Katy looks up again and her finger resumes touching the screen, but now only the iPad counts the numbers (Figure 1b): she no longer says them aloud herself. After 'seventeen', several fingers fall on the screen at once, and then 'twenty-one' is heard (since she has tapped the screen with several fingers, only the sound of the final number is said aloud, but the four discs all appear under where she has touched). This produces a pause in the action, and Katy's lips spread into a smile. All but the index finger are tucked away, as the rhythmic tapping continues along with the chorus of named numbers. At 'twenty-seven' Katy looks up, no longer watching the screen (see Figure 1c), and she continues swiping and saying numbers. This continues until a finger accidentally land on Reset. Katy's fingeras the main organ of touch in this encountertakes on new capacities through the reset button. It is no longer the organ that can only move or drag the yellow circle. The power of the reset button to recalibrate the tempo and rhythm of this encounter, becomes part of the finger's potentiality, thereby redefining what is currently entailed in the sense of touch.

Discussion

Fingers can serve as both a physical extension of what Rotman (1987) calls the 'one-who-counts' (p. 27) (usually with an extended pointed finger reaching out to the world) as well as the thing-tobe-counted (in which the gaze is directed towards one's own fingers): fingers are thus simultaneously subject and object, both of the person and of the world (Alibali & diRosso, 1999). And this is what makes the finger actions of Katy so interesting; the mathematical act of counting with TouchCounts fuses this duality and in so doing changes the relationship between the hand and eye, as well as the ears.

Katy's hand actions change over the course of the episode, not only in the particular muscular form they take, first sliding down the screen as if lingering on the yellow discs to produce or partake in their falling off the screen, and then tapping impetuously so that each new touching of the screen follows the end of the sounds of the voiced numerical. The swiping gesture seems more exploratory while the tapping gesture seems to concatenate into a unit the touch-see-hear bundle of sensations involved in making a new disc-numeral-name. As Streeck writes, tapping is also "characteristic of ritualized behavior" (p. 76), which suggests that Katy has moved from exploration to practice. In both the swiping and the tapping, the finger can be seen as making an indexical gesture, with the trace being both visible and audible, not to mention tangible for Katy.

Although the initial movement and touch of her finger is what produces the disc, it is the disc that drives the swiping movement of her finger. Indeed, both her finger and her eyes follow the yellow disc as it heads down the screen. In shepherding the numbered disc off the screen, Katy sees when it's time to lift her finger and start making a new disc. But with the tapping, the eyes attend to the numerical sign on the disc-indeed, when 10 appears, Katy notices the change from the previous one-digit numerals. In this sense, the eye and the finger do very similar things in the swiping, the visible trace is followed closely by Katy's eyes as the swiping takes place, so that the hand is subordinated to the watchful eye. With the tapping, the hand seems less subordinated, with the eye only interested when there's a novel situation. When Katy looks up, the hand is no longer subordinate. When Katy's eyes close, her fingers do the seeing and touching as they repetitively tap. But of course, there is more than the eye and hand involved in this situation. The ear and voice feature importantly as well. Indeed, while the voice is subordinate to the touch (it only speaks while Katy taps), Katy's hand is also subordinate to the ear in that the ear judges the moment of the next tap. And the ear is disrupted by the hand, when several fingers touch the screen at once, causing the voice to jump from "seventeen" to "twenty-one." The eye, which was about to drift off, must return to survey the situation. And the hand returns to its single digit tapping. The importance of the aural and the vocal in this context is interesting in terms of the counting activity at play. Indeed, the ritual origins of counting are oral in nature, and counting with young children is often undertaken as the learning of a song that one memorises and chants. The involvement of the hand in this otherwise oral event provides a visual and tangible trace of the count, while also associating each counted number with a single swipe or a single tap.

One might question whether Katy's actions on the screen, which we might think of as touchpointing, can really be thought of as gestures. Streeck argues that such touch-pointing gestures (and indeed all gestures) emerge from the touching and handling of things-the tracing (or other "datagathering devices" such as caressing, probing, cupping) of objects that allows one to discover its texture and temperature (and, for young children, for instance, the difference between a cylinder and a pyramid). When the hand has done its exploring of the object, which fulfills an epistemic function in gathering information, it may then be lifted off the object and inclined to repeat the same movements 'in the air': "the hands' data-gathering methods are used as the basis for gestural communication" (p. 69). Streeck identifies such gestures as being communicative, which for him is the characteristic feature of a gesture. So perhaps Katy's touch-pointing becomes a gesture once she lifts her hand form the screen to do her tapping.

Distinguishing hand movements that explore from ones that communicate is problematic though. As Streeck writes, exploratory actions can become communicative when they are made visible to others, who may join in the action or infer tactile properties. If we look at Katy's swiping and tapping gestures, we might say that they are both exploratory, with the swiping gestures involving prolonged tactile contact that enables her to discover what would happen when her finger touches the glass-that a yellow disc would appear, with a numeral on it; that the disc would move down the screen; that the iPad would speak the numeral's name aloud, and that this could all be repeated as often as she wished. But Katy's swiping and, later, her tapping, are also communicative inasmuch as they tell TouchCounts what to do and say. The same might be said for clicks of the mouse or key presses of the keyboard, with the difference that the touchscreen is acted upon by direct hand motions. Instead of disentangling the tracing from the pointing (the exploration from the communication), we suggest that re-assembling them into an indexical enables us to see how Katy's hand movements can tap into the potentiality of the body by reconfiguring the relationships between sensations of touch, sight and sound that are at play. This potentiality mobilizes new mathematical meanings as Katy uses her fingers to count on, to count with and to count out one by one and indefinitely. Streeck recognises that hand-gestures "enable translations between the senses" (p. 70) as tactile discoveries provide visual information for interlocutors. With Katy though, the tactile discoveries provide visual and auditory information to herself. She is her own interlocutor.

Conclusion

Streeck argues that hand-gestures cannot be taken only as components of a language system cast apart from the material world and used only to communicate about the world. Rather, they are of the world, and part of how we feel the world around us. This perspective requires us to see the moving hand as "environmentally coupled" [START_REF] Goodwin | Environmentally coupled gestures[END_REF], that is, as inextricable from the things it touches and engages with. But while Streeck implies a vector from the exploratory hand action to the communicative hand-gesture, our case studies reveal how the exploratory hand frees itself from the optic regime and invents meaning as much as it communicates it. This new kind of gesture is possible in large part because of the feedback mechanism of digital technologies, which can talk, push and show back. With the touchscreen interface, and particularly the multitouch actions, the hand is involved in a process of communicating that is also a process of inventing and interacting.

In the example we presented, we have shown that the gestures made by Katy in TouchCounts had an indexical nature both because they involved some kind of pointing (with one finger or more) and they left a trace that is both visible and audible. The trace is important in drawing attention to the material engagement of the gestures. The gestures arise out of movements of the hand, but they also result in material reconfigurations that can give rise to new movements of the hand. In discussing the effect of new digital technologies in mathematics, Rotman has written about the future cultural neoteny in which speech would "become reconfigured (as it was once before when transformed by alphabetic writing), re-mediated and transfigured into a more mobile, expressive, and affective apparatus by nascent gesturo-haptic recourses" (p. 49). We interpret these speculative comments as an indication that the future of the gesturing hand in relation to new media may involve all sorts of surprises, and that perhaps even pre-school children may count 'on their hands' to 100 as they engage with these media.

Figure 1

 1 Figure 1(a). Katy swiping; (b) Following the yellow disc; (c) Tapping while looking up.

Proceedings of CERME10


domain: math shs

text:
Laura Broley
email: l_brole@live.concordia.ca

Chantal Buteau
email: cbuteau@brocku.ca

Eric Muller
email: emuller@brocku.ca

(Legitimate peripheral) computational thinking in mathematics

Keywords: Computational thinking, mathematicians' practices, legitimate peripheral participation

Computational thinking" is a hot topic in math education, among teachers whose curricula now include the term, and researchers who wish to pinpoint what it means and how it could be promoted in classrooms. A recent study resulted in a theoretical model of the computational practices of professional mathematicians and scientists, with the aim of offering teachers a set of competencies around which to build activities for their students. Nonetheless, concrete examples that validate the model and exemplify its use in math classrooms have yet to be discussed. We wish to open up this discussion, which we see as crucial to understanding how to empower students to participate in the computational thinking that has become integral to the mathematics community and beyond.

Introduction

Parallel to the invention of the personal computer, [START_REF] Papert | Mindstorms: Children, computers, and powerful ideas[END_REF] envisioned a world where children fluently use the tool as young mathematicians. Some thirty years later, we've witnessed a widespread resurgence of interest in that vision, taking shape in educational reforms (e.g., in Europe; [START_REF] Bocconi | Developing computational thinking in compulsory education: Implications for policy and practice[END_REF] and research regimes (cf., www.ctmath.ca) in the name of computational thinking, deemed a 21 st century skill. Yet, there is little consensus on what this "new" term encompasses or how/if it should be conceptualized within subject areas beyond computer science [START_REF] Grover | Computational thinking in K-12: A review of the state of the field[END_REF]. In response to these issues, [START_REF] Weintrop | Defining computational thinking for mathematics and science classrooms[END_REF] developed a taxonomy of computational thinking practices geared towards science and mathematics. They based their work on a literature review, an analysis of learning activities, and interviews with "biochemists, physicists, material engineers, astrophysicists, computer scientists, and biomedical engineers" (p. 134). They also show, through concrete examples, how the practices might be promoted in physics, biology, and chemistry classrooms. To build on this work, we could ask: What might the computational thinking practices look like in mathematics classrooms? Moreover, are they representative of professional mathematicians' practices?

In this contribution, we attempt to provide some answers to these questions by drawing on two resources: 1) fifteen years of experience in a sequence of three undergraduate Mathematics Integrated with Computers and Applications (MICA) courses at Brock University, where students create and use computer environments to explore mathematics concepts or real-world situations; and 2) reflections of mathematicians whose research falls within an area recognized by the European Mathematical Society in 2011: "Together with theory and experimentation, a third pillar of scientific inquiry of complex systems has emerged in the form of […] modeling, simulation, optimization, and visualization" (p. 2). The next section outlines the perspective underlining our work and our approach in preparing this paper. We then present our results, i.e., we exemplify (empowering legitimate peripheral) computational thinking practices in mathematics.

Theory and methods

The way we interpret "Learning mathematics with technology" in the context of this paper is well explained by [START_REF] Lave | Situated learning: Legitimate peripheral participation[END_REF] concept of "legitimate peripheral participation", whereby students are invited to become mathematicians through engaging in their shared practices. "Mathematics", then, is not seen as a body of knowledge to be acquired by the student, but rather as a social community to which the student gradually gains membership. Hence, we do not discuss computer "technology" from a cognitive point of view, for example, as a helpful tool in illustrating concepts. We focus, instead, on how mathematicians, the old-timers of their discipline, and students, the new-comers, create and use computer tools to engage in practices considered to be integral to the mathematical community. In recent work, [START_REF] Weintrop | Defining computational thinking for mathematics and science classrooms[END_REF] outline what they believe to be these integral practices (Figure 1). Their framework provides a detailed description, specific to STEM (i.e., science, technology, engineering, and mathematics), of one of three dimensions introduced by [START_REF] Brennan | New frameworks for studying and assessing the development of computational thinking[END_REF] to characterize "computational thinking": namely, computational concepts, practices, and perspectives. Such frameworks seek to elaborate on the general definitions on which they are grounded; for instance, that of Cuny, Snyder, and Wing, who describe computational thinking as "[t]he thought processes involved in formulating problems and their solutions so that the solutions are represented in a form that can be effectively carried out by an information-processing agent" (2010). Computer programming plays a particularly important role, as it "is not only a fundamental skill of [computer science] and a key tool for supporting the cognitive tasks involved in [computational thinking] but a demonstration of computational competencies as well" (Grover & Pea, 2013, p. 40). Such ideas invoked in us vivid images of our own experiences with/as mathematicians and students creating and using computer tools to do mathematics. And this inspired us to address an apparent void: that is, a comparative picture that highlights the powerful computational thinking employed by professional mathematicians, on the one hand, and, on the other, the potential of students to participate in the same kind of thinking.

To prepare this picture, we re-examined [START_REF] Broley | La programmation informatique dans la recherche et la formation en mathématiques au niveau universitaire[END_REF] research, which explored the use of programming by 14 mathematicians in their research and teaching. In an interview, each participant described research where they developed and used computer tools. Unbeknownst to us at the time, this provided examples of how some full-membership mathematicians engage in computational thinking. Amongst them, we chose four that align with the groupings in Weintrop et al.'s (2016) taxonomy. We then reconsidered the data from another study [START_REF] Buteau | Undergraduate mathematics students appropriating programming as a tool for modelling, simulation, and visualization: A case study[END_REF] the 14 MICA projects completed by one student, Ramonaas a source of four examples of peripheral computational thinking. MICA's goal of responding to society's need for professionals proficient in programmable technology made it a natural database for comparison.

Results

This section provides examples of computational thinking as it might be experienced by full and peripheral participants in the mathematics community. For each category identified by [START_REF] Weintrop | Defining computational thinking for mathematics and science classrooms[END_REF], we describe a mathematician's project that we feel effectively exemplifies it. This is contrasted to a MICA project that we see as providing access to the same kind of practices.

Data practices

Adèle uses her expertise in mathematics and computing to solve problems in financial engineering. In one project, she developed a model that enables investors to judge the investment potential of various market entities. In particular, the model calculates the risk that an investor will lose money because the investee is unable to pay back what they owe. The tricky part is that most investees have never had such financial problems (e.g., with bankruptcy). To assess a given company or individual, Adèle considers their portfolio: She collects their history of actions (e.g., investments, bonds, shares) on the financial market. The basic idea is that as others agreed to invest a certain amount of money in the company or individual, they implicitly demanded to be compensated for the risks they were taking, thereby predicting the probability that the investment would be a good one. Mathematically-speaking, the problem is of an extremely high dimension: Adèle's model contains over 20 parameters that must be estimated for each portfolio by manipulating the corresponding data with optimization techniques. Intensive numerical methods are then applied to the specified model to generate the data necessary for evaluating the risk of the investee(s) being considered. The result is not a simple measure of the average risk. Adèle must perform a nuanced analysis to meet her clients' needs, calculating and visualizing probability distributions in order to portray the best and worst case scenarios. About the place of computation in her work, Adèle was blunt: She said there would be no project without it. In fact, when tasked with assessing the risk associated to hundreds of companies at once, she must use computer clusters to get the job done.

In their second of three MICA courses, students in Ramona's cohort were assigned a project similar to Adèle's. During lectures, they were introduced to mathematical ideas related to the stock market. In regards to programming, they also learned how to read data from files. Up to this point, they had worked with data they created through simulation; but during this project, they had to use data from Stock Market sources. During two (two-hour) lab sessions, the students initiated their individual work by collecting the S&P index, a measure of market conditions, from 1950 to 2002, and writing a program to manipulate, visualize, and analyze the data using standard statistical techniques. Students were also required to select ten stocks and, like Adèle, make recommendations to a fictive client based on their own analysis. In her report, Ramona grounded her recommendation on the mean and average yearly percentage of her stock selection. Then, as requested, she conducted a regression analysis of a stock over a decade and described how visualizing the data as a cloud of points confirmed her interpretation of the coefficient as representing a weak correlation.

Modelling and simulation practices

Alice's projects are often inspired by a collaborator in need of her modelling and simulation skills. She spoke, for example, of a kinesiologist who initiated a multi-year project about muscles. Alice began by learning about the application, which she knew little about. She could then design a system of equations that would allow her to study the features of interest, i.e., tensions, bulges, and fibers; but only once the model was implemented on a computer. During her interview, Alice joked that computation was essential because, unfortunately, the solution to a real-world mathematical model never simplifies to the quadratic formula. While some researchers use existing simulators to gain access to their models' solutions, Alice prefers to have the control of constructing her own. This comes at a price: Even if her team starts with an existing code, they still have to think very hard about how they implement their equations, import data, generate meshes, and so on. But all this hard work apparently paid off in this project: Alice described the resulting computational model as "the most complex simulator of its kind", and was hesitant to share its massive code during her interview. This tool was used systematically to investigate issues the researchers initially sought out to understand. But by varying parameters in an exploratory mode, they also found and tested solutions to an unreported problem: the forming of well-defined fiber structures. During her interview, it was clear that Alice was excited by this discovery, for her collaborator had observed the formation of the exact same fiber structures, but in a real human! In the end, the data collected during this ultrasound experiment of a person on a bicycle assessed Alice's model, confirming that it represented "the real thing" in more ways than expected. Modelling and simulation practices that resemble Alice's are central to the MICA courses. At the end of the third course, students in Ramona's cohort were asked to use the theory of cellular automata to model and simulate the spread of an epidemic. Students worked individually to construct the computational model (i.e., to implement it in VB.Net), complete with a dynamic visualization of the cellular automatum and a complementary graph (Figure 2, left). Using this model, students were invited to observe real-time simulations of certain scenarios with the goal of coming to understand the effects of vaccination on the proliferation and diminution of epidemics. They were then told how to extend their models to include the cost of immunization and medical treatment, so to find (estimate) the solution of a minimal medical cost problem. In her report, Ramona went beyond finding the solution; as required, she also assessed the ability of her extended computational model to provide an accurate estimate, finishing with suggestions for improvement.

Computational problem solving practices

To understand Norman's pure mathematics research, some preparation is in order. In his work, a permutation of length n is just a string, σ = σ1σ2…σn, where each σi is a unique element from the set {1, 2, …, n}; for example, α = 624531 is a permutation of length 6. Given another permutation, e.g. β = 231, we say that ∝ contains the pattern β if we can find in ∝ a subsequence (not necessarily consecutive) whose numbers have the same relative order as 231. The fact that ∝ contains the subsequence 451 -1 is the smallest number, 5 is the highest, and 4 is in betweenmeans that it contains β (we could have equally used subsequences 241, 251, 231, or 453). If a permutation does not contain a pattern, it is said to avoid it; for instance, α avoids 1234. An interesting problem for mathematicians is to determine the number of permutations pn of length n that avoid a given pattern. It is known that pn grows almost exponentially with n. The growth rate, however, is still unknown for many patterns. In search of one such rate, Norman's team had to build a complex computer tool. The programming was delegated to a student, whose life was simplified by the development of a modular solution based on an existing subroutine for another pattern. The creation of the entire algorithm, nonetheless, was a team effort, for it involved the careful assessment of different approaches and solutions. One option was to calculate the exact value of pn for as many n as possible and then extrapolate the growth rate. But according to Norman, this approach was inefficient: At the time of his project, they could calculate the exact values only for n ≤ 25, which was not enough to provide an acceptable solution. The mathematicians hence chose a probabilistic approach that uses estimates for pn rather than exact values. This enabled them to calculate more data points; but their program was still slow. Seeking to troubleshoot and debug the problem, Norman suggested that his team try to visualize the permutations. Their decision to represent a permutation σ = σ1σ2…σn as a function that sends i to σi led to the discovery of an unexpectedly striking structure (Figure 3,left). Norman insisted on the importance of creating this particular computational abstraction: The pattern would not have been observable, for example, had they produced only a list of matrix entries. And then Norman might have missed out on a novel research direction that occupied him for many years.

Since all MICA projects involve programming, computational problem solving practices like Norman's always form a major part of their completion. Starting in the first MICA course, students discuss what makes a math problem amenable to exploration through programming. Since this is new to most of them, they are also led to develop their computational skills through a carefully selected progression of projects, which increase in complexity in terms of both the mathematical content and the programming requirements. For example, Ramona and her peers learned about discrete dynamical systems alongside techniques of displaying graphics in VB.Net, which they applied by creating a program to numerically and graphically explore the logistic map. In a later project, the students were asked to build on this work (i.e., borrow modular computational solutions from it) and program a tool to explore the system of a two-parameter cubic (Figure 2,right). This new problem required more serious preparation for a computational solution, as the domain of the cubic called for the consideration of different cases. Inherent to the programming process was also troubleshooting and debugging, creating computational abstractions, and assessing different kinds of solutions, which may have contributed to Ramona's conclusion in her written report that "creating and working with this program has assisted me to fully grasp the way a dynamical system works by observing the table, the graphs, and the cobweb with countless test values."

Systems thinking practices

Albert has studied many complex systems, including those defined in celestial mechanics. The three-body problem, for example, seeks to describe the motion of a spaceship in the presence of two bodies, like the Earth and its moon. The complexity of the system is managed by ignoring the presence of other bodies, taking the spaceship to have negligible mass, and assuming that the massive bodies move in circular orbits. These explicit boundaries do not render the system useless.

In fact, the model has provided initial approximations for real space missions. Moreover, it serves as a rich source of problems that allow Albert to show off the mathematically and numerically sophisticated software he has developed, software that according to him can compute "amazing things" that are simply "not computable" by traditional methods. Albert's team has computed the uncomputable at different levels. Macroscopically-speaking, they have investigated the three-body system as a whole by finding and classifying an infinity of its periodic solutions (i.e., closed trajectories where a spaceship could remain in orbit). On a microscopic level, they have explored these orbits in family groups and individually. This latter consideration also helps them understand some relationships between elements within the system: For a given orbit, the researchers can determine the set of trajectories that a spaceship could follow after experiencing a slight perturbation. The resulting tube-like structures are like highways that enable space travel to faraway places with minimal effort (and money). One image (Figure 3, right) is enough to convey the importance of visualization in communicating Albert's results.

In each MICA course, the last two weeks are dedicated to challenging original projects wherein students select topics of interest to them. Ramona's terminal (14 th ) project is an example of how students might engage in practices similar to Albert's and, as the MICA course creators aimed, "develop their own strategies for handling complex real world problems" (Buteau et al., 2016, p. 144). With two of her colleagues, Ramona investigated, as a whole, the complex system associated to the water level changes in Lake Erie (Canada). In particular, they were interested in explaining how and why the level changes over time (i.e., in understanding the relationships within the system). They described their initial research in existing literature as "a crucial starting point in [their] project, allowing [them] to obtain an understanding for the changes in the water supply of Lake Erie." Based on the information gathered, they designed and programmed stochastic and deterministic models of the phenomenon. They then performed an analysis, through simulation, of six case studies, representing the system in various ways on a different, more microscopic, level. They used their initial research to justify the assumptions they made, the parameters they chose, and the case studies they considered in order to manage the complexity of the system. This explanation was part of the 26-page report where Ramona's group communicated their results.

Discussion and conclusions

The four pairs of examples provided above aim to render Weintrop et al.'s (2016) framework more concrete, validate its correspondence with a diverse set of authentic professional practices, and provide some insight as to how students might be invited to gain access to them, all within the context of mathematics. Ramona's work differed from the mathematicians' in its magnitude: Her projects were more restricted in scope and length, her computer programs were more naïve, and her findings had less immediate value for the community at large. This is not surprising since Ramona was in a peripheral phase of participating in the mathematics community, where she was simultaneously negotiating entrance into a community of students at a particular university, with its own norms limiting engagement in full-membership mathematical activity. Nonetheless, in exposing Ramona to the computational practices of mathematicians, programs like MICA support a nuanced discussion of what it means to integrate digital tools in students' learning of mathematics.

Many scholars have reported on the ways in which building and/or interacting with digital tools might assist students in meaningfully acquiring mathematical ideas or ways of thinking that are embedded in current curricula. The collection of papers presented in the working group on learning mathematics with technology at this year's CERME conference provides numerous examples. In fact, the main framework used in this paper was built on the premise that learning activities involving computational thinking practices can enrich students' understanding of mathematics and science [START_REF] Weintrop | Defining computational thinking for mathematics and science classrooms[END_REF]. This said, the framework was equally inspired by the everincreasing computational nature of STEM-related disciplines. As evidenced by our examples, and much work that precedes us, the power of the computer has had a major impact on the way that STEM professionals (can) do their work. And so, the computational thinking trend presents an opportunity (or perhaps a necessity) for mathematics educators at all levels to reconsider not just the "how" of mathematics teaching, but also the "what", i.e., the knowledge and skills to be taught. After all, students' participation in the computational thinking practices of mathematicians might not just prepare them for a computational future in general; it may also widen their perspectives of the nature of mathematics and who is capable of learning (and doing) it.

Both research and experience tell us that reflecting on the above issues, developing curricula to address them, and enacting that curricula in classrooms are quite different feats. Detailed and extensive frameworks like the one developed by [START_REF] Weintrop | Defining computational thinking for mathematics and science classrooms[END_REF] can certainly help support researchers, curricula developers, and teachers. But there is still a need to examine more closely and completely the experiences of students who are peripheral participants in computational communities of practice: What skilled knowledge (i.e., practices) do they actually develop? Moreover, how do they identify with communities they are both entering and (eventually) influencing? Given our analysis in this paper, the MICA program provides a rich context within which to study such questions. The answers could lead to an enlightening discussion about challenges and opportunities in bringing about a nuanced technology-rich mathematics education.

Figure 1 :

 1 Figure 1: Computational Thinking Practices, taken from Weintrop et al., 2016, p. 135

Figure 2 :

 2 Figure 2: Ramona's epidemic simulator (left) and discrete dynamical system program (right)

Figure 3 :

 3 Figure 3: Norman's discovery of structure in pattern-avoiding permutations (left) and Albert's computation of trajectories resulting from a perturbation off an orbit close to the moon (right)

Proceedings of CERME10


Paul Strohmeier
email: p.strohmeier@di.ku.dk

Cedric Honnet
email: cedric@honnet.eu

To improve haptic experiences in VR and AR, we must first improve tracking.

Context

Haptic feedback technologies have become incredibly sophisticated. Using intricate measuring and actuating devices, users can feel, in real time, the physical forces of a microscopic probe hitting the surface of a drop of water, before being pulled inside by its surface tension [START_REF] Mohand Ousaid | Feeling what an insect feels[END_REF]. Using pre-recorded data, it is possible to simulate the texture of arbitrary materials as a pen moves over a flat surface [START_REF] Romano | Creating realistic virtual textures from contact acceleration data[END_REF]. Using simple physics models it is possible for users to asses the weight and compliance of a virtual object [START_REF] Schorr | Fingertip Tactile Devices for Virtual Object Manipulation and Exploration[END_REF].

A plethora of devices have been designed to support haptic output in VR and AR [START_REF] Pacchierotti | Wearable Haptic Systems for the Fingertip and the Hand: Taxonomy, Review, and Perspectives[END_REF]. There appears to be an unspoken assumption that -similar to the various head-mounted displays that we use today -we will one day have devices that allow us to touch virtual worlds in the manner that we now have visual access to them. These devices are often designed as special purpose output devices, aimed at providing the user with distinct sensations such as compliance, texture, shear force or a caress. Such output focused devices however seem to ignore a key difference between touch and visual perception. I see things distributed in space. To an extent the proximity of my eye to the object I am looking at is irrelevant. In contrast, if I touch an object, I feel the touch where it occurs. The only way I can perceive an object through the sense of touch is to reach out and perform the action of touch. If one wishes to present a visual virtual world, this can be done without precise knowledge of what the user is looking at. If, however, one wishes to present a virtual world of touch at the user's fingertips, the touch perceptions can only be represented if one has precise information of the touch action performed by the user.

Existing VR platforms track the position of hands or hand-held objects poorly. Commercial VR systems such as the HTC or Oculus Rift can have significant missalignment between the position of their controllers and their virtual counterparts. Using hand-tracking systems such as leap motion can create uncanny experiences as the hand is almost tracked, or grotesque distortions when the physical hand is oriented in a way that fails to meet the trackers assumptions. Reaching and grasping for objects using AR glasses such as the Meta 2 can be an exercise of guessing where the system believes ones hand to be and acting accordingly.

Touch is both an action and a sensation. To render a texture [START_REF] Romano | Creating realistic virtual textures from contact acceleration data[END_REF], material properties [START_REF] Schorr | Fingertip Tactile Devices for Virtual Object Manipulation and Exploration[END_REF], or physical forces [START_REF] Mohand Ousaid | Feeling what an insect feels[END_REF] one needs to precisely understand the action performed to provide an appropriate response. Current systems, that do this well, operate in a constrained environment. We believe that, now, a major challenge is to develope better tracking and input technologies, to fully leverage existing haptic output devices.

Our Research Background

Paul Strohmeier's first exploration of haptics was for a telerobotics project (Figure 1). The mediated touch system consisted of robotic puppet with an actuated head [START_REF] Strohmeier | Exploring Bodies, Mediation and Points of View using a Robotic Avatar[END_REF]. Eight capacitive touch sensors were also placed on the robotic puppet. A 'remote user' could log into the system by wearing a system consisting of vibration motors and video goggles. When the 'remote user' would move their head, so would the robotic puppet. The video goggles allowed the user to see what the robot saw. Each sensor activated the corresponding vibration motor attached to the body of the robot. When the vibration motors were set to either be on or off, remote users felt like 'there were phones buzzing on [their] body' or 'like [they are] a door, and there is somebody ringing all the doorbells'. Participants preferred a non-binary condition, were the information of the approach behavior was encoded in the intensity of the feedback. Playing with this system made the importance of carefully designing the input for touch communication apparent. Paul revisited haptic feedback again through his work with flexible displays. With colleagues from the Human Media Lab at Queen's University Paul presented a flexible smartphone, Reflex [START_REF] Strohmeier | ReFlex: A Flexible Smartphone with Active Haptic Feedback for Bend Input[END_REF]. Reflex measures the strain placed on its display and uses this information to generate haptic feedback. Difference in sensing fidelity of prototype iterations further underlined the importance of precise measures and high temporal synchronization between measures and actuation.

Together with Kasper Hornbaek, Paul further investigated the parameter space of feedback generated by user motion. For example, they used a linear slider and a recoil-type transducer [START_REF] Yao | Design and analysis of a recoil-type vibrotactile transducer[END_REF] for adding textures to the slider movement. Using this setup they explored how changing feedback parameters changed the experience of the users [START_REF] Strohmeier | Generating Haptic Textures with a Vibrotactile Actuator[END_REF]. A follow up study added the same actuator to a pointing device, similar to those used in contemporary VR setups. Using optical tracking, the pointer was augmented with 'inair-textures'. They conducted a study that explored how changing what aspects of a movement are used to generate a texture changes how it is perceived [START_REF] Strohmeier | From Pulse Trains to "Coloring with Vibrations[END_REF] (Figure 2).

Cedric Honnet originally started working with tangible interfaces at Sifteo, the company emerging from the Siftables [START_REF] Merrill | Siftables: towards sensor network user interfaces[END_REF] project. At Sifteo he worked on firmware, software and R&D projects, but in his free time he developed various applications including position-aware games or tangible music interfaces. He took this work from San Francisco back to Paris where he co-founded Tangible Display (TD) and expanded his work on designing spatially aware systems. Systems designed by TD used their own patented markers to track the absolute position and orientation of tangible controllers on interactive surfaces.

Similar systems had become quite popular with musicians, for example, Bjoerk famously used the Reactable in her 2007 world tour. Some of the systems developed by Tangible Display were also deployed for playing and performing music (Figure 3). When placed on the interactive surface, tangible pucks come to life. However, once lifted, they 'vanish' in terms of their interactive ability and transform back into generic noninteractive objects. Bothered by this limitation, Cedric started adding inertial measurement units (IMUs) to the pucks, to track their trajectories once lifted off the surface.

This work eventually led to a stand-alone inertial tracker, called Twiz1 . The Twiz consists of a 9DOF IMU and a microcontroller with integrated Bluetooth (Figure 4). The Twiz was used in various HCI explorations, including playful explorations that sample the movement of the things around us [START_REF] Schlegel | From Ordinary to Expressive Objects Using Tiny Wireless IMUs[END_REF][START_REF] Schlegel | Movement of Things Exploring Inertial Motion Sensing When Autonomous, Tiny and Wireless[END_REF].

In interest of easier integration with VR and AR systems and to facilitate embedded haptic systems Cedric is working on the HIVE tracker [START_REF] Quiñones | HIVE Tracker: a tiny, lowcost, and scalable device for sub-millimetric 3D positioning[END_REF], a system that merges the approach previously explored with the laser positioning of the HTC Vive Lighthouse system. Using the Lighthouse signal to correct for drift, and the inertial data for fine-grained movement, the HIVE tracker can report its position and movement with submillimeter precision.

Future Work

We are interested in combining our knowledge of haptic feedback design and position tracking to create an embedded self-contained haptic input and output device. We envision a general purpose platform that combines high resolution tracking with a haptic actuator and driving circuitry, as well as wireless communication. We hope to participate in the in-touch workshop to help understand how to position our future work. We are especially interested in discussions regarding the concept of 'embodied interaction' as used by the tangibles research communities and how it relates to the concept of 'transparency' as used by the robotics communities. We are further interested in how insights on the design of 'embodied' or 'transparent' systems might be used to provide access to information about the world that we typically do not have access to.

Figure 1 -

 1 Figure 1 -Telerobotic System for exploring Mediated Touch [9].

Figure 2 -

 2 Figure 2 -Participant testing input parameters for rendering of nongrounded mid-air textures [10].

Figure 3 -

 3 Figure 3 -Performer using TD's tangible controller system with Ableton Live

Figure 4 -

 4 Figure 4 -Twiz (Tiny, Wireles, IMUz) in 3d printed enclosure.

https://www.hackster.io/cedric/twiz-da5c63


Pascal Fontaine
email: pascal.fontaine@loria.fr

Mizuhito Ogawa
email: mizuhito@jaist.ac.jp

Thomas Sturm
email: thomas.sturm@loria.fr

Van Khanh To

Xuan Tung Vu

Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Quantifier-free non-linear real arithmetic (QF NRA) appears in many applications of satisfiability modulo theories (SMT) solving. Efficient reasoning techniques for the corresponding constraints in SMT solvers is thus highly relevant. Examples of SMT solvers with theory reasoners for non-linear real arithmetic are CVC4 [START_REF] Cimatti | Satisfiability modulo transcendental functions via incremental linearization[END_REF], SMT-RAT [START_REF] Florian | SMT-RAT: An SMT-Compliant nonlinear real arithmetic toolbox[END_REF], Z3 [START_REF] Jovanović | Solving non-linear arithmetic[END_REF] and Yices [START_REF] Dutertre | Yices 2.2[END_REF]. We report here on the prototypical non-linear theory reasoner in veriT. It is based on three techniques, namely interval constraint propagation, subtropical satisfiability, and quantifier elimination. Interval constraint propagation and subtropical satisfiability are heuristic procedures that are easy to implement, but incomplete. Completeness of the theory solver is guaranteed by the use of quantifier elimination. In order to make optimal use of existing knowledge and work in the symbolic computation community, we take advantage of an independent computer algebra system (Redlog/Reduce). The theory reasoner built from these three components is called lazily, on full models produced by the underlying SAT solver. This simple SMT solver is actually quite efficient in solving problems in the QF NRA category of the SMT-LIB.

The order of authors is strictly alphabetic.

In Section 2, we briefly present the three procedures that are used in the tool. We then describe how they are combined into one theory reasoner for non-linear real arithmetic literals. We finally report on experiments on the SMT-LIB.

Component Procedures

Interval Constraint Propagation

This section briefly introduces Interval Constraint Propagation (ICP) [START_REF] Benhamou | Continuous and interval constraints[END_REF], a technique providing an incomplete but efficient method to check the satisfiability over the reals of a finite set of polynomial constraints [START_REF] Fränzle | Efficient solving of large nonlinear arithmetic constraint systems with complex boolean structure[END_REF][START_REF] Ratschan | Efficient solving of quantified inequality constraints over the real numbers[END_REF][START_REF] Gao | Satisfiability modulo ODEs[END_REF][START_REF] Khanh | SMT for polynomial constraints on real numbers[END_REF][START_REF] Tung | rasat: an SMT solver for polynomial constraints[END_REF]. Algorithm 1 depicts a naive version of ICP. This algorithm works on boxes in R n ; initially (line 2) there is one box set to ] -∞, ∞[ n for the n variables in the constraints. It iteratively (line 3) picks one box B (line 4) and uses the constraints to heuristically contract that box (line 6), then it evaluates the constraints on B, discarding the box if there is no possible solution (one constraint is unsatisfiable on the box, line 7), or decomposing B into smaller boxes, which will later be considered the same way (line 12). The algorithm terminates concluding unsatisfiability (line 15) when all boxes have been discarded (one constraint is unsatisfiable, for each box), or concluding satisfiability when all constraints are valid in the same box (line 10, indeed every point in the box is a solution for the set of constraints). Note that ICP does not require tedious computations with real algebraic numbers at all. However, the algorithm does not necessarily terminate since it might infinitely decompose boxes into smaller ones.

Algorithm 1 ICP for a set of polynomial constraints ϕ Our implementation of ICP uses testing [START_REF] Khanh | SMT for polynomial constraints on real numbers[END_REF][START_REF] Tung | rasat: an SMT solver for polynomial constraints[END_REF], to improve satisfiability detection: the constraints are regularly checked for satisfiability on random test points inside given boxes. Since ICP uses interval arithmetic as an approximation to check validity or unsatisfiability of constraints on a box of full dimension, it is rarely able to find satisfiable assignments in presence of equations. Our ICP algorithm furthermore uses the Intermediate Value Theorem as a heuristic to assert that equations are satisfied within a given box [START_REF] Tung | rasat: an SMT solver for polynomial constraints[END_REF].

Subtropical Satisfiability

The subtropical satisfiability checking method [START_REF] Fontaine | Subtropical satisfiability[END_REF] (SUBTROP) is based on the simultaneous evaluation of the input set of polynomial constraints when the values of variables approach 0, 1, or ∞ following some polynomial curve. It basically checks for such limits, if within each polynomial one monomial dominates all other ones. If so, the algorithm computes an interpretation for variables, based on the curve, such that all polynomials in the set have a value of a given sign. The method is mostly limited to determine the satisfiability of a set of constraints containing only inequalities, but it appears that this is useful for the various applications represented in the SMT-LIB.

Example 1. Consider f 1 = -12 + 2x 12 y 25 z 49 -31x 13 y 22 z 110 -11x 1000 y 500 z 89 and f 2 = -23 + 5xy 22 z 110 -21x 15 y 20 z 1000 + 2x 100 y 2 z 49 , and the satisfiability checking problem

f 1 > 0 ∧ f 2 > 0.
The method (see [START_REF] Fontaine | Subtropical satisfiability[END_REF] for details) shows that the monomials 2x 12 y 25 z 49 and 5xy 22 z 110 respectively dominate in f 1 and f 2 when (x, y, z) tends to (0, ∞, 0), more precisely, for values

(x, y, z) = (a n 1 , a n 2 , a n 2 ) with, for instance, n 1 = -238834 120461 , n 2 = 2672460 1325071 , n 3 = -368561
1325071 and a sufficiently large. The method actually computes those n 1 , n 2 , and n 3 . So, if a ∈ R + is large enough, then both constraints f 1 (a n 1 , a n 2 , a n 3 ) > 0 and f 2 (a n 1 , a n 2 , a n 3 ) > 0 are satisfied. Consider a = 2 for instance: then f 1 (a n 1 , a n 2 , a n 3 ) ≈ 16371.99 and f 2 (a n 1 , a n 2 , a n 3 ) ≈ 17707.27.

The subtropical method expresses as linear constraints some conditions for one monomial to dominate within a polynomial. Subsequently, an SMT solver is used to check the satisfiability of these linear constraints. If the linear constraints are satisfiable, then the non-linear constraint is satisfiable and the model of the linear constraints provides a witness for the polynomial curve, i.e., for the previous example, the values of n 1 , n 2 , and n 3 . For sets of polynomial constraints, the process is essentially the same.

Experimentally, the application of the subtropical satisfiability method to solve nonlinear constraints is fast, either to succeed or to fail. On our experiments, it furthermore provides an answer on several problems that defeat all state-of-the-art solvers. The method thus establishes a useful complementing heuristic with little drawback, to be used either upfront or in portfolio with other approaches to deal with non-linear constraints.

Quantifier Elimination

As a complete method, we use Quantifier Elimination techniques (QE). While it is possible to quickly implement ICP and subtropical satisfiability checking, those quantifier elimination techniques are significantly more complex and require expertise. It is not feasible to implement a custom version for SMT with a few person months. We thus used a computer algebra system, namely Reduce, and more precisely, the package Redlog [START_REF] Dolzmann | Redlog: Computer algebra meets computer logic[END_REF] which implements interpreted first-order logic on top of computer algebra. Besides many other domains, Redlog provides decision procedures for real closed fields. For real arithmetic Redlog combines two quantifier elimination techniques, virtual substitution [START_REF] Weispfenning | The complexity of linear problems in fields[END_REF][START_REF] Weispfenning | Quantifier elimination for real algebra-the quadratic case and beyond[END_REF][START_REF] Košta | New Concepts for Real Quantifier Elimination by Virtual Substitution[END_REF] with partial cylindrical algebraic decomposition [START_REF] Collins | Partial cylindrical algebraic decomposition for quantifier elimination[END_REF][START_REF] Seidl | Cylindrical Decomposition Under Application-Oriented Paradigms[END_REF]. For a survey of real applications of Redlog see [START_REF] Sturm | A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications[END_REF]. Further theories supported by Redlog include discretely valued fields [START_REF] Sturm | Linear problems in valued fields[END_REF], term algebras [START_REF] Sturm | Quantifier elimination in term algebras[END_REF], QBF [START_REF] Seidl | Boolean quantification in a first-order context[END_REF][START_REF] Sturm | Parametric quantified SAT solving[END_REF], Presburger Arithmetic [START_REF] Lasaruk | Weak quantifier elimination for the full linear theory of the integers. A uniform generalization of Presburger arithmetic[END_REF] and fragments of non-linear integer arithmetic [START_REF] Lasaruk | Weak integer quantifier elimination beyond the linear case[END_REF].

To embed a decision procedure in SMT, one property is mandatory: the procedure should feature small conflict production. From an unsatisfiable set of literals, it should produce an unsatisfiable subset containing few unnecessary literals, optimally a minimal unsatisfiable subset, i.e. such that all proper subsets are satisfiable. With small conflict production, the SMT infrastructure goes considerably beyond a SAT solver enumerating all possible models of the Boolean abstraction of the input formula, the theory reasoner refuting them one at a time. We recently presented [START_REF] Jaroschek | Adapting real quantifier elimination methods for conflict set computation[END_REF] a method using linear optimization to compute conflict sets for cylindrical algebraic decomposition and virtual substitution. Virtual substitution and cylindrical algebraic decomposition share the same basic idea of finding a finite set of test points that suffice to determine the unsatisfiability of a set of constraints S . If the set S is unsatisfiable, each of these test points falsifies at least one constraint in S . Finding a conflict set reduces to finding a subset of the constraints that contains, for each test point, at least one unsatisfied constraint. We implemented this in the Quantifier Elimination algorithms in Redlog. Redlog/Reduce now furthermore provides an interface for SMT solver, so that the software can be used as a theory reasoner with little effort. This reasoner is used in our portfolio of tools, and guarantees the completeness of the combination of reasoners on real closed fields.

Combining Procedures

We have previously discussed subtropical satisfiability (SUBTROP), interval constraint propagation (ICP), and quantifier elimination (QE). Our aim is to combine these in a complete and efficient framework for solving polynomial constraints. Recall that SUB-TROP is only an incomplete heuristics, and ICP does not even guarantee termination; ICP might loop forever, for instance in the case of touching spheres. Combining ICP sequentially with other procedures thus requires heuristics for ICP termination to ensure fairness and to let the other algorithms also work on the constraints. Before decomposing a box into smaller ones (line 12 in Algorithm 1), our algorithm will check if bounded boxes have been generated, all the bounded boxes are smaller than a chosen value ε in all dimensions. If so, the algorithm gives up, and returns UNKNOWN along with the box B resulting from the contraction of ] -∞, ∞[ n from constraints; the algorithm returns the empty box in case of unsatisfiability and the valid box in case of satisfiability. Intuitively, B is an over-approximation of all boxes possibly containing solutions of constraints. We furthermore require that boxes are handled in a chronological order, that is, S in Algorithm 1 becomes a queue, where the first box (the oldest one) is chosen and removed, and newer boxes are added at the end. Boxes are decomposed only along axes with lengths greater than ε. The procedure ensures unbounded boxes are not decomposed infinitely. The algorithm terminates either when it detects satisfiability (or unsatisfiability) or all bounded boxes have all dimensions smaller than ε. We refer to this terminating version of ICP as ICPT.

A lazy combining approach considers the procedures as black boxes and invokes them sequentially to check the satisfiability of the constraints. The fastest procedures to terminate are ordered first, and the complete procedure is called last. In Algorithm 2, SUBTROP(ϕ) returns SAT if and only if subtropical satisfiability succeeds in finding a model for ϕ; remember that subtropical satisfiability is indeed essentially a model finding method. The complete decision procedure (in our case, quantifier elimination methods as implemented in Redlog/Reduce) is called in line 9, and returns SAT (resp. UNSAT) if the input is satisfiable (resp. unsatisfiable). Notice that, when calling the complete decision procedure, the set of constraints ϕ is complemented with a box B found by ICPT. Actually (this is not shown in Algorithm 2), ϕ is furthermore cleaned of the constraints that are valid in the box B.

Algorithm 2 Lazy combination of procedures

1: function LAZY(ϕ) 2:
if SUBTROP(ϕ) = SAT then 3:

return SAT 4:

end if 5:

(result, B) ← ICPT(ϕ) 6:

if result = UNKNOWN then 7:

return result 8:

end if 9:

return QE (ϕ ∧ B) 10: end function

We experimentally evaluated another combination interleaving more tightly the complete procedure and ICP. The combination is similar to ideas in [START_REF] Loup | A symbiosis of interval constraint propagation and cylindrical algebraic decomposition[END_REF]: when a box of ICP becomes smaller than a threshold ε, quantifier elimination is called, for the sake of completeness, to solve the remaining unknown constraints over this small box. We found however that this performs less well than the lazy one above. We are investigating further techniques to fix this.

Experiments

All experiments were conducted on an Intel Xeon E5-2680v2 at 2.80GHz running GNU/Linux CentOS 6.4 with kernel 2.6.32. Each solver ran on the 11354 benchmarks of the QF NRA category (quantifier-free Non-linear Real Arithmetic) of the SMT-LIB (4963 are labeled as satisfiable, 5296 unsatisfiable, 1095 unknown) with a memory limit of 8 GB memory and a time out of 2500 seconds for each benchmark.5 In our implementation, raSAT [START_REF] Khanh | SMT for polynomial constraints on real numbers[END_REF][START_REF] Tung | rasat: an SMT solver for polynomial constraints[END_REF] serves as the ICP-based solver, the computer algebra system Redlog/Reduce [START_REF] Dolzmann | Redlog: Computer algebra meets computer logic[END_REF] for quantifier elimination, and STROPSAT [START_REF] Fontaine | Subtropical satisfiability[END_REF] as the implementation of subtropical satisfiability. The interface for the three tools within veriT is 900 lines of C code. Notice that CVC4 is used inside STROPSAT to solve linear constraints (see again [START_REF] Fontaine | Subtropical satisfiability[END_REF]). The framework for solving polynomial constraints in the SMT solver is called lazily, when the underlying SAT solver has produced a full model and if the corresponding set of literals is not shown unsatisfiable by the linear arithmetic decision procedure in veriT.

Table 1 compares the performance of the distinct procedures and their combination. Notice that QE alone already solves many problems, but combining the procedures brings improvements both in running time and in the number of solved problems. SUB-TROP increases the number of solved satisfiable problems and improves times for several satisfiable problems, without significantly impacting negatively for the problems solved by the other methods: indeed, SUBTROP actually takes around 2000 additional seconds for six difficult problems also solved by the combination of ICP and QE, and uses 4000 seconds to solve 17 more problems. ICP has a general positive impact both on running times and on the number of problems solved. Table 2 compares state-of-the-art SMT solvers with support for non-linear arithmetic. SMT-RAT implements a less lazy combination (as mentioned in the previous section) between interval constraint propagation and cylindrical algebraic decomposition [START_REF] Loup | A symbiosis of interval constraint propagation and cylindrical algebraic decomposition[END_REF], Yices and Z3 implement the nlsat procedure [START_REF] Jovanović | Solving non-linear arithmetic[END_REF]. CVC4 uses contextdependent simplification [START_REF] Reynolds | Designing theory solvers with extensions[END_REF] and incremental linearization [START_REF] Cimatti | Satisfiability modulo transcendental functions via incremental linearization[END_REF]. Our results validate the main point of the paper: a combination of simple heuristics (ICP and subtropical satisfiability) with quantifier elimination as implemented in a computer algebra system (Redlog/Reduce) slightly tuned to fit the SMT infrastructure is an efficient decision procedure to solve non-linear arithmetic SMT problems. Table 2 also clearly exhibits that the virtual best solver -a portfolio of all mentioned solvers running in parallel -is much better than each individual solver; we attribute this to the variety of techniques used in the solvers.

Conclusion

Implementing state-of-the-art decision procedures for the theory of real non-linear arithmetic requires a lot of expertise and is very time consuming. Hopefully, reusing a computer algebra system actually provides good results on the SMT-LIB. We also notice that, thanks to the diversity of techniques used to tackle this theory, the various SMT solvers have complementary strengths and the virtual best solver is much better than each solver alone.

We expect the non-linear arithmetic reasoner in veriT to improve, following the improvements in the embedded computer algebra system itself. For instance, Redlog/Reduce features a new experimental virtual substitution algorithm which shows very promising results on problems stemming from other computer algebra applications; veriT will eventually benefit from this new algorithm once it becomes stable.

In future works, we plan to investigate a less lazy combination of ICP and quantifier elimination. In our current prototype, the quantifier elimination is applied for each box that ICP is unable to discard, one at a time. The idea would be, with a single call to quantifier elimination, to eliminate several boxes in ICP.

Table 1 .

 1 Numbers of benchmarks solved by component procedures

	Benchmarks SUBTROP	ICP	QE	All	w/o SUBTROP	w/o ICP	w/o QE
	SAT	1936 4302 4400 4450	4433 4436 4313
	UNSAT	2530 4472 4959 5012	5012 4959 4472
	Total (11354)	4466 8774 9359 9462	9445 9395 8785
	Total time (s)	4744 18835 67945 50632	44815 67420 22357

Table 2 .

 2 Performance of state-of-the-art SMT solvers on QF NRA

	Benchmarks	CVC4 SMT-RAT	Z3	Yices veriT	veriT only	Virtual best
	SAT	2929	4398 4905	4845 4450	18	5183
	UNSAT	5324	4425 5038	5120 5012	1	5744
	Total (11354)	8253	8823 9943	9965 9462	19 10927
	Total time (s) 146154	57787 37740 132137 50632 11706 119998

See http://www.jaist.ac.jp/ ∼ s1520002/veriT+STROPSAT+raSAT+Redlog/ for full results and the tool with the source code. Note to reviewers: this will soon be on Zenodo.

Acknowledgments

This project has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689 (SC 2 ), and from the European Research Council under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Xuan Tung Vu would like to acknowledge the JAIST Off-Campus Research Grant for fully supporting him during his stay at LORIA, Nancy. The work has also been partially supported by the JSPS KAKENHI Grant-in-Aid for Scientific Research(B) (15H02684) and the JSPS Core-to-Core Program (A. Advanced Research Networks).