, the complexity of deducing a set of constraint-sets from e and ? using our inference system. We obtain the complexity by solving the following set of recursive equations

I. (,-?)-=-i($v,

, ?) = 1 + |split(?)| × max (?1,?2)?split(?) (I(e 1 , ? 1 ) + I

, <?>{e}</?> : element n {? }), ?) = 2 + I

+. , AnyElt) * ) + I(e 2 , ?) + I

, $v in e 1 return e 2 , ?) = 1 + I(e 2 , ?) + I

×. , + 5)) + N (e 2 , ?) × 2 O(T (e2,?)) + N

, The cases of let-expressions and for-loop expressions include the complexity of satisfiability checks for the inferred type for the bound variable

, Lastly, we state the worst-case time complexity of our backward type inference for the XQuery core

, Assume we are given an XQuery expression e and its output type ?. Then the set of solvable constraint-sets is computed in 2 O(2 (|e|+1) |?|) time by our inference system

C. and C. , Since the size of the largest type in S is O(2 |e| |?|) by Lemma 5.7, for each constraint-set C in S , its satisfiability can be tested in 2 O(2 |e| |?|) time by the decision procedure in, |e| |?|) time by Lemma 5.9

?. ,

. C\-$v-c-\-$v, , p.0

, By induction hypothesis on (9) with (11) and (13), we have

+. , .. .. , +. Then, and ;. .. From, there exists j such that (15) f 1 ,. .. , f j?1 ? C ($v) * and thus f k ? C ($v) where k = 1,. .. , j ? 1 750 (16) f j ? C($v) (17) f j+1 ,. .. , f n ? C ($v) * and thus f k ? C ($v) where k = j + 1, Assume Quant(?) = 1. The case where Quant(?) = + is similarly proved using the following property: ?

, Unlike the type inference for XPath axes, the type inference for the XQuery core is only sound and not 760 complete, mainly because of the approximation introduced for for-loop expressions. From the soundness and the decidability of the inference system, From (20) and (21)

, Let e be an XQuery expression with the only free variable $doc, which denotes an input document. Let ? i be an input type (the type for $doc) and ? o an output type, Then there exists an algorithm that says yes if S ? e : ? o and ?C ? S such that C = {?} and ? i <: C($doc)

S. Boag, D. Chamberlin, M. Fernández, D. Florescu, J. Robie et al.,

. Language, W3C Recommendation, 2010.

H. Hosoya, J. Vouillon, and B. C. Pierce, Regular expression types for XML, ACM Trans. Program. Lang. Syst, vol.27, issue.1, pp.46-90, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00009271

D. Draper, M. Dyck, P. Fankhauser, M. Fernández, A. Malhotra et al., , p.895

, XQuery 1.0 and XPath 2.0 Formal Semantics, 2010.

J. Clark and S. Derose, XML Path Language (XPath) Version 1.0, W3C Recommendation, 1999.

A. Berglund, S. Boag, D. Chamberlin, M. F. Fernández, M. Kay et al., W3C Recommendation, 2010.

J. Robie, D. Chamberlin, M. Dyck, and J. Snelson, XML Path Language (XPath) 3.0, W3C Recommendation, 2014.

J. Robie, D. Chamberlin, M. Dyck, and J. Snelson, XQuery 3.0: An XML Query Language, W3C Recommendation, 2014.

D. Colazzo and C. Sartiani, Precision and complexity of XQuery type inference, Proceedings of the 13th 910 International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming, pp.89-100, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00626217

A. Tozawa, Towards static type checking for XSLT, ACM Symposium on Document Engineering, pp.18-27, 2001.

T. Milo, D. Suciu, and V. Vianu, Typechecking for XML transformers, Journal of Computer and System, vol.915, issue.1, pp.66-97, 2003.

T. Perst and H. Seidl, Macro forest transducers, Inf. Process. Lett, vol.89, issue.3, pp.141-149, 2004.

S. Maneth, A. Berlea, T. Perst, and H. Seidl, XML type checking with macro tree transducers, Proceedings of the Twenty-fourth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database

, Systems, PODS '05, pp.283-294, 2005.

A. Tozawa, XML type checking using high-level tree transducer, Proceedings of the 8th International Symposium on Functional and Logic Programming, FLOPS '06, pp.81-96, 2006.

A. Frisch and H. Hosoya, Towards practical typechecking for macro tree transducers, Proceedings of the 925 11th International Conference on Database Programming Languages, DBPL'07, pp.246-260, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00126895

J. Engelfriet and H. Vogler, Macro tree transducers, Journal of Computer and System Sciences, vol.31, issue.1, pp.90066-90068, 1985.

J. Engelfriet, The time complexity of typechecking tree-walking tree transducers, Acta Informatica, vol.930, issue.2, pp.139-154, 2009.

G. Castagna, H. Im, K. Nguyen, and V. Benzaken, A core calculus for XQuery 3.0: Combining navigational and pattern matching approaches, Proceedings of the 24th European Symposium on Programming, pp.232-256, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01104872

G. Huet, The zipper, J. Funct. Program, vol.7, issue.5, pp.549-554, 1997.

P. Genevès and N. Gesbert, XQuery and static typing: Tackling the problem of backward axes, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp.88-100, 2015.

P. Genevès, N. Laya¨?dalaya¨?da, and A. Schmitt, Efficient static analysis of XML paths and types, Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 940 '07, pp.342-351, 2007.

N. Alon, T. Milo, F. Neven, D. Suciu, and V. Vianu, XML with data values: typechecking revisited, Journal of Computer and System Sciences, vol.66, issue.4, pp.688-727, 2003.

H. Hosoya and B. C. Pierce, XDuce: A statically typed XML processing language, ACM Trans. Internet Technol, vol.3, issue.2, pp.117-148, 2003.

M. Murata, D. Lee, M. Mani, and K. Kawaguchi, Taxonomy of XML schema languages using formal language theory, ACM Trans. Internet Technol, vol.5, issue.4, pp.660-704, 2005.

R. M. Amadio and L. Cardelli, Subtyping recursive types, ACM Trans. Program. Lang. Syst, vol.15, issue.4, pp.575-631, 1993.
URL : https://hal.archives-ouvertes.fr/inria-00070035

A. Brüggemann-klein and D. Wood, One-unambiguous regular languages, Information and Computation 950, vol.140, pp.229-253, 1998.

P. Genevès, N. Laya¨?dalaya¨?da, A. Schmitt, and N. Gesbert, Efficiently deciding µ-calculus with converse over finite trees, ACM Trans. Comput. Logic, vol.16, issue.2, p.41, 2015.

A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types, J. ACM, vol.55, issue.4, p.1391293, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00336120

S. Heubach and T. Mansour, Combinatorics of Compositions and Words, 2009.

V. Benzaken, G. Castagna, and A. Frisch, CDuce: An XML-centric general-purpose language, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP '03, pp.51-63, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00152619

A. Møller and M. I. Schwartzbach, The design space of type checkers for XML transformation languages, Proceedings of the 10th International Conference on Database Theory, ICDT '05, pp.17-36, 2005.

V. Benzaken, G. Castagna, H. Hosoya, B. C. Pierce, and S. Vansummeren, Encyclopedia of Database Systems, pp.3646-3650, 2009.

S. Hakuta, S. Maneth, K. Nakano, and H. Iwasaki, IEEE 30th International Conference on Data Engineering, ICDE '14, pp.952-963, 2014.

A. Aho and J. Ullman, Translations on a context free grammar, Information and Control, vol.19, issue.5, pp.90706-90712, 1971.
DOI : 10.1145/800169.805425

D. Olteanu, H. Meuss, T. Furche, and F. Bry, XPath: Looking forward, in: XML-Based Data Management and Multimedia Engineering-EDBT, pp.109-127, 2002.

D. Olteanu, Forward node-selecting queries over trees, ACM Trans. Database Syst, vol.32, issue.1
DOI : 10.1145/1206049.1206052
URL : http://web.comlab.ox.ac.uk/oucl/work/dan.olteanu/papers/INFOSYS-TR-2005-5.pdf

A. Møller, M. O. Olesen, and M. I. Schwartzbach, Static validation of XSL transformations, ACM Trans. Program. Lang. Syst, vol.29, issue.4

J. Clark, XSL Transformations (XSLT) Version 1.0, W3C Recommendation, 1999.

V. Benzaken, G. Castagna, D. Colazzo, and K. Nguyen, Optimizing XML querying using type-based docu980 ment projection, ACM Trans. Database Syst, vol.38, issue.1, p.4, 2013.
DOI : 10.1145/2445583.2445587
URL : http://arxiv.org/pdf/1104.2079

M. Benedikt and J. Cheney, Semantics, types and effects for XML updates, Proceedings of the 12th International Symposium on Database Programming Languages, DBPL '09, pp.1-17, 2009.
DOI : 10.1007/978-3-642-03793-1_1
URL : http://homepages.inf.ed.ac.uk/jcheney/publications/drafts/w3c-update-types-tr.pdf

J. Robie, D. Chamberlin, M. Dyck, D. Florescu, J. Melton et al., XQuery Update Facility 1.0, 985 W3C recommendation, 2011.

M. Benedikt and J. Cheney, Destabilizers and independence of XML updates, Proc. VLDB Endow, vol.3, issue.1-2, pp.906-917, 2010.
DOI : 10.14778/1920841.1920956
URL : http://www.comp.nus.edu.sg/%7Evldb2010/proceedings/files/papers/R81.pdf

N. Klarlund and A. Møller, MONA Version 1.4 User Manual, BRICS, 2001.

P. Genevès and N. Laya¨?dalaya¨?da, Deciding XPath containment with MSO, Data Knowl. Eng, vol.63, issue.1, pp.108-136, 2007.

J. Doner, Tree acceptors and some of their applications, Journal of Computer and System Sciences, vol.4, issue.5, pp.80041-80042, 1970.

M. Benedikt and H. Vu, Higher-order functions and structured datatypes, Proceedings of the 15th 995 International Workshop on the Web and Databases, pp.43-48, 2012.

N. Gesbert, P. Genevès, and N. Laya¨?dalaya¨?da, Parametric polymorphism and semantic subtyping: The logical connection, Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, pp.107-116, 2011.
DOI : 10.1145/2034574.2034789
URL : https://hal.archives-ouvertes.fr/inria-00585686