{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:59:20Z","timestamp":1762459160851,"version":"3.41.2"},"reference-count":33,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T00:00:00Z","timestamp":1344556800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Unravelings are transformations from a conditional term rewriting system\n(CTRS, for short) over an original signature into an unconditional term\nrewriting systems (TRS, for short) over an extended signature. They are not\nsound w.r.t. reduction for every CTRS, while they are complete w.r.t.\nreduction. Here, soundness w.r.t. reduction means that every reduction sequence\nof the corresponding unraveled TRS, of which the initial and end terms are over\nthe original signature, can be simulated by the reduction of the original CTRS.\nIn this paper, we show that an optimized variant of Ohlebusch's unraveling for\na deterministic CTRS is sound w.r.t. reduction if the corresponding unraveled\nTRS is left-linear or both right-linear and non-erasing. We also show that\nsoundness of the variant implies that of Ohlebusch's unraveling. Finally, we\nshow that soundness of Ohlebusch's unraveling is the weakest in soundness of\nthe other unravelings and a transformation, proposed by Serbanuta and Rosu, for\n(normal) deterministic CTRSs, i.e., soundness of them respectively implies that\nof Ohlebusch's unraveling.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:4)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":4,"title":["Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Naoki","family":"Nishida","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6234-0161","authenticated-orcid":false,"given":"Masahiko","family":"Sakai","sequence":"additional","affiliation":[]},{"given":"Toshiki","family":"Sakabe","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,8,10]]},"reference":[{"key":"10.2168\/LMCS-8(3:4)2012_ABH03","doi-asserted-by":"crossref","unstructured":"S. Antoy, B. Brassel, and M. Hanus. Conditional narrowing without conditions. InProceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 20-31, ACM Press, 2003.","DOI":"10.1145\/888251.888255"},{"key":"10.2168\/LMCS-8(3:4)2012_ALS94","doi-asserted-by":"crossref","unstructured":"J. Avenhaus and C. Lor\u00eda-S\u00e1enz. On conditional rewrite systems with extra variables and deterministic logic programs. InProceedings of the 5th International Conference on Logic Programming and Automated Reasoning, volume 822 ofLecture Notes in Computer Science, pages 215-229, Springer, 1994.","DOI":"10.1007\/3-540-58216-9_40"},{"key":"10.2168\/LMCS-8(3:4)2012_BN98","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow.Term Rewriting and All That. Cambridge University Press, United Kingdom, 1998.","DOI":"10.1017\/CBO9781139172752"},{"issue":"3","key":"10.2168\/LMCS-8(3:4)2012_BK86","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J. A. Bergstra and J. W. Klop","year":"1986","journal-title":"Journal of Computer and System Sciences"},{"key":"10.2168\/LMCS-8(3:4)2012_tata2007","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, C. L\u00f6ding, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on: http:\/\/www.grappa.univ-lille3.fr\/tata, 2007. Release October 12th, 2007."},{"issue":"1-2","key":"10.2168\/LMCS-8(3:4)2012_DO90","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0304-3975(90)90064-O","volume":"75","author":"N. Dershowitz and M. Okada","year":"1990","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(3:4)2012_DLMMU04","doi-asserted-by":"crossref","unstructured":"F. Dur\u00e1n, S. Lucas, J. Meseguer, C. March\u00e9, and X. Urbain. Proving termination of membership equational programs. In N. Heintze and P. Sestoft, editors,Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, pages 147-158, ACM, 2004.","DOI":"10.1145\/1014007.1014022"},{"key":"10.2168\/LMCS-8(3:4)2012_GM87","doi-asserted-by":"crossref","unstructured":"E. Giovannetti and C. Moiso. Notes on the elimination of conditions. In S. Kaplan and J.-P. Jouannaud, editors,Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, volume 308 ofLecture Notes in Computer Science, pages 91-97, Springer, 1987.","DOI":"10.1007\/3-540-19242-5_8"},{"key":"10.2168\/LMCS-8(3:4)2012_GGS10","unstructured":"K. Gmeiner, B. Gramlich, and F. Schernhammer. On (un)soundness of unravelings. In C. Lynch, editor,Proceedings of the 21st International Conference on Rewriting Techniques and Applications, volume 6 ofLeibniz International Proceedings in Informatics, pages 119-134, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2010."},{"key":"10.2168\/LMCS-8(3:4)2012_GGS12","unstructured":"K. Gmeiner, B. Gramlich, and F. Schernhammer. On soundness conditions for unraveling deterministic conditional rewrite systems. In A. Tiwari, editor,Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12), volume 15 ofLeibniz International Proceedings in Informatics, pages 193-208, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, May 2012."},{"issue":"3","key":"10.2168\/LMCS-8(3:4)2012_Kap87","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(87)80010-X","volume":"4","author":"S. Kaplan","year":"1987","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"10.2168\/LMCS-8(3:4)2012_Luc98","volume":"1998","author":"S. Lucas","year":"1998","journal-title":"Journal of Functional and Logic Programming"},{"issue":"4","key":"10.2168\/LMCS-8(3:4)2012_LMM05","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1016\/j.ipl.2005.05.002","volume":"95","author":"S. Lucas, C. March\u00e9, and J. Meseguer","year":"2005","journal-title":"Information Processing Letters"},{"key":"10.2168\/LMCS-8(3:4)2012_Mar96","doi-asserted-by":"crossref","unstructured":"M. Marchiori. Unravelings and ultra-properties. In M. Hanus and M. Rodr\u00edguez-Artalejo, editors,Proceedings of the 5th International Conference on Algebraic and Logic Programming, volume 1139 ofLecture Notes in Computer Science, pages 107-121, Springer, 1996.","DOI":"10.1007\/3-540-61735-3_7"},{"key":"10.2168\/LMCS-8(3:4)2012_Mar97","unstructured":"M. Marchiori. On deterministic conditional rewriting. Computation Structures Group, Memo 405, MIT Laboratory for Computer Science, 1997."},{"key":"10.2168\/LMCS-8(3:4)2012_MH94","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF01190830","volume":"5","author":"A. Middeldorp and E. Hamoen","year":"1994","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"10.2168\/LMCS-8(3:4)2012_Nishida04phd","unstructured":"N. Nishida.Transformational Approach to Inverse Computation in Term Rewriting. Doctor thesis, Graduate School of Engineering, Nagoya University, Nagoya, Japan, 2004."},{"key":"10.2168\/LMCS-8(3:4)2012_NS09entcs","doi-asserted-by":"crossref","unstructured":"N. Nishida and M. Sakai. Completion after program inversion of injective functions. In A. Middeldorp, editor,Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming, volume 237 ofElectronic Notes in Theoretical Computer Science, pages 39-56, Elsevier, 2009.","DOI":"10.1016\/j.entcs.2009.03.034"},{"key":"10.2168\/LMCS-8(3:4)2012_NSS03entcs","doi-asserted-by":"crossref","unstructured":"N. Nishida, M. Sakai, and T. Sakabe. Narrowing-based simulation of term rewriting systems with extra variables and its termination proof. In G. Vidal, editor,Proceedings of the 12th International Workshop on Functional and (Constraint) Logic Programming, volume 86 ofElectronic Notes in Theoretical Computer Science, Issue 3, pages 1-18, Elsevier, 2003.","DOI":"10.1016\/S1571-0661(04)80693-5"},{"key":"10.2168\/LMCS-8(3:4)2012_NSS04ss","unstructured":"N. Nishida, M. Sakai, and T. Sakabe. On simulation-completeness of unraveling for conditional term rewriting systems. IEICE Technical Report SS2004-18, the Institute of Electronics, Information and Communication Engineers, volume 104, no. 243, pages 25-30, 2004."},{"key":"10.2168\/LMCS-8(3:4)2012_NSS05rta","doi-asserted-by":"crossref","unstructured":"N. Nishida, M. Sakai, and T. Sakabe. Partial inversion of constructor term rewriting systems. In J. Giesl, editor,Proceedings of the 16th International Conference on Rewriting Techniques and Applications, volume 3467 ofLecture Notes in Computer Science, pages 264-278, Springer, 2005.","DOI":"10.1007\/978-3-540-32033-3_20"},{"key":"10.2168\/LMCS-8(3:4)2012_NSS05ieice","unstructured":"N. Nishida, M. Sakai, and T. Sakabe. Generation of inverse computation programs of constructor term rewriting systems.IEICE Transactions on Information and Systems, J88-D-I(8):1171-1183, 2005 (in Japanese)."},{"key":"10.2168\/LMCS-8(3:4)2012_NSS11rta","unstructured":"N. Nishida, M. Sakai, and T. Sakabe. Soundness of unravelings for deterministic conditional term rewriting systems via ultra-properties related to linearity. In M. Schmidt-Schau\u00df, editor,Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, volume 10 ofLeibniz International Proceedings in Informatics, pages 267-282, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2011."},{"issue":"1-2","key":"10.2168\/LMCS-8(3:4)2012_Ohl01","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/s002000100064","volume":"12","author":"E. Ohlebusch","year":"2001","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"10.2168\/LMCS-8(3:4)2012_Ohl02","doi-asserted-by":"crossref","unstructured":"E. Ohlebusch.Advanced Topics in Term Rewriting. Springer, 2002.","DOI":"10.1007\/978-1-4757-3661-8"},{"key":"10.2168\/LMCS-8(3:4)2012_Ros04","doi-asserted-by":"crossref","unstructured":"G. Rosu. From conditional to unconditional rewriting. In J. L. Fiadeiro, P. D. Mosses, and F. Orejas, editors,Revised Selected Papers of the 17th International Workshop on Recent Trends in Algebraic Development Techniques, volume 3423 ofLecture Notes in Computer Science, pages 218-233, Springer, 2004.","DOI":"10.1007\/978-3-540-31959-7_13"},{"key":"10.2168\/LMCS-8(3:4)2012_SG07","unstructured":"F. Schernhammer and B. Gramlich. On proving and characterizing operational termination of deterministic conditional rewrite systems. In D. Hofbauer and A. Serebrenik, editors,Proceedings of the 9th International Workshop on Termination, pages 82-85, 2007."},{"issue":"7","key":"10.2168\/LMCS-8(3:4)2012_SG10","first-page":"659","volume":"79","author":"F. Schernammer and B. Gramlichh","year":"2010","journal-title":"The Journal of Logic and Algebraic Programming 2010."},{"key":"10.2168\/LMCS-8(3:4)2012_SR06","doi-asserted-by":"crossref","unstructured":"T.-F. Serbanuta and G. Rosu. Computationally equivalent elimination of conditions. In F. Pfenning, editor,Proceedings of the 17th International Conference on Rewriting Techniques and Applications, volume 4098 ofLecture Notes in Computer Science, pages 19-34, Springer, 2006.","DOI":"10.1007\/11805618_3"},{"key":"10.2168\/LMCS-8(3:4)2012_SR06b","doi-asserted-by":"crossref","unstructured":"T.-F. Serbanuta and G. Rosu. Computationally equivalent elimination of conditions. Technical Report UIUCDCS-R-2006-2693, University of Illinois at Urbana-Champaign, 2006.","DOI":"10.1007\/11805618_3"},{"key":"10.2168\/LMCS-8(3:4)2012_SMI95","doi-asserted-by":"crossref","unstructured":"T. Suzuki, A. Middeldorp, and T. Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In J. Hsiang, editor,Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 ofLecture Notes in Computer Science, pages 179-193, Springer, 1995.","DOI":"10.1007\/3-540-59200-8_56"},{"key":"10.2168\/LMCS-8(3:4)2012_Toy87","doi-asserted-by":"crossref","unstructured":"Y. Toyama. Confluent term rewriting systems with membership conditions. In S. Kaplan and J.-P. Jouannaud, editors,Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, volume 308 ofLecture Notes in Computer Science, pages 228-241, Springer, 1987.","DOI":"10.1007\/3-540-19242-5_17"},{"issue":"3","key":"10.2168\/LMCS-8(3:4)2012_Vir99","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1006\/jsco.1999.0288","volume":"28","author":"P. Viry","year":"1999","journal-title":"Journal of Symbolic Computation"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/669\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/669\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:53:38Z","timestamp":1681242818000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/669"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,10]]},"references-count":33,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:4)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1206.5694","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1206.5694","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"arxiv","id":"1701.00650","asserted-by":"subject"},{"id-type":"doi","id":"10.4204\/eptcs.235.5","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arxiv.1701.00650","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,8,10]]},"article-number":"669"}}