Abstract
The inversion method proposed by Glück and Kawabe uses grammar programs as intermediate results that comprise sequences of operations (data generation, matching, etc.). The determinization method used in the inversion method fails for a grammar program of which the collection of item sets causes a conflict even if there exists a deterministic program equivalent to the grammar program. In this paper, by ignoring shift/shift conflicts, we improve the determinization method so as to cover grammar programs causing shift/shift conflicts. Moreover, we propose a method to eliminate infeasible definitions from unfolded grammar programs and show that the method succeeds in determinizing some grammar programs for which the original method fails. By using the method as a post-process of the original inversion method, we make the original method strictly more powerful.
This work has been partially supported by MEXT KAKENHI #21700011.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramov, S.M., Glück, R.: Principles of inverse computation in a functional language. In: APLAS 2000, pp. 141–152 (2000)
Abramov, S., Glück, R.: The universal resolving algorithm: Inverse computation in a functional language. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 187–212. Springer, Heidelberg (2000)
Abramov, S.M., Glück, R.: The universal resolving algorithm and its correctness: inverse computation in a functional language. Sci. Comput. Program. 43(2-3), 193–229 (2002)
Almendros-Jiménez, J.M., Vidal, G.: Automatic partial inversion of inductively sequential functions. In: Horváth, Z., Zsók, V., Butterfield, A. (eds.) IFL 2006. LNCS, vol. 4449, pp. 253–270. Springer, Heidelberg (2007)
Dershowitz, N., Mitra, S.: Jeopardy. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 16–29. Springer, Heidelberg (1999)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Glück, R., Kawabe, M.: A program inverter for a functional language with equality and constructors. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 246–264. Springer, Heidelberg (2003)
Glück, R., Kawabe, M.: A method for automatic program inversion based on LR(0) parsing. Fundam. Inform. 66(4), 367–395 (2005)
Glück, R., Kawabe, M.: Revisiting an automatic program inverter for Lisp. SIGPLAN Notices 40(5), 8–17 (2005)
Glück, R., Kawada, Y., Hashimoto, T.: Transforming interpreters into inverse interpreters by partial evaluation. In: Proceedings of Partial Evaluation and Semantics-based Program Manipulation, pp. 10–19. ACM Press (2003)
Gries, D.: The Science of Programming. Springer, Heidelberg (1981)
Harrison, P.G.: Function inversion. In: Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation, pp. 153–166. North-Holland (1988)
Harrison, P.G., Khoshnevisan, H.: On the synthesis of function inverses. Acta Inf. 29(3), 211–239 (1992)
Hullot, J.M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)
Kawabe, M., Futamura, Y.: Case studies with an automatic program inversion system. In: Proceedings of the 21st Conference of Japan Society for Software Science and Technology, 6C-3, pp. 1–5 (2004)
Kawabe, M., Glück, R.: The program inverter LRinv and its structure. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2005. LNCS, vol. 3350, pp. 219–234. Springer, Heidelberg (2005)
Khoshnevisan, H., Sephton, K.M.: InvX: An automatic function inverter. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 564–568. Springer, Heidelberg (1989)
Korf, R.E.: Inversion of applicative programs. In: Proceedings of the 7th International Joint Conference on Artificial Intelligence, pp. 1007–1009. William Kaufmann (1981)
Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95(4), 446–453 (2005)
Matsuda, K., Mu, S.-C., Hu, Z., Takeichi, M.: A grammar-based approach to invertible programs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 448–467. Springer, Heidelberg (2010)
McCarthy, J.: The inversion of functions defined by Turing machines. In: Automata Studies, pp. 177–181. Princeton University Press (1956)
Nagashima, M., Sakai, M., Sakabe, T.: Determinization of conditional term rewriting systems. Theor. Comput. Sci. 464, 72–89 (2012)
Nishida, N., Sakai, M.: Completion after program inversion of injective functions. In: Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming. ENTCS, vol. 237, pp. 39–56 (2009)
Nishida, N., Sakai, M., Sakabe, T.: Generation of inverse computation programs of constructor term rewriting systems. The IEICE Trans. Inf. & Syst. J88-D-I(8), 1171–1183 (2005) (in Japanese)
Nishida, N., Sakai, M., Sakabe, T.: Partial inversion of constructor term rewriting systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 264–278. Springer, Heidelberg (2005)
Nishida, N., Sakai, M., Sakabe, T.: Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity. Logical Methods in Computer Science 8(3), 1–49 (2012)
Nishida, N., Vidal, G.: Program inversion for tail recursive functions. In: Schmidt-Schauß, M. (ed.) RTA 2011. LIPIcs, vol. 10, pp. 283–298. Schloß Dagstuhl–Leibniz-Zentrum für Informatik (2011)
Nishida, N., Vidal, G.: Computing more specific versions of conditional rewriting systems. In: Albert, E. (ed.) LOPSTR 2012. LNCS, vol. 7844, pp. 137–154. Springer, Heidelberg (2013)
Ohlebusch, E.: Advanced topics in term rewriting. Springer, Heidelberg (2002)
Romanenko, A.: The generation of inverse functions in Refal. In: Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation, pp. 427–444. North-Holland (1988)
Romanenko, A.: Inversion and metacomputation. In: Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 12–22. ACM Press (1991)
Schernhammer, F., Gramlich, B.: VMTL–A modular termination laboratory. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 285–294. Springer, Heidelberg (2009)
Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination proofs for logic programs by term rewriting. ACM Trans. on Comput. Log. 11(1), 1–52 (2009)
Secher, J.P., Sørensen, M.H.: From checking to inference via driving and dag grammars. In: Proceedings of Partial Evaluation and Semantics-Based Program Manipulation, pp. 41–51. ACM Press (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Niwa, M., Nishida, N., Sakai, M. (2013). Improving Determinization of Grammar Programs for Program Inversion. In: Albert, E. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2012. Lecture Notes in Computer Science, vol 7844. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38197-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-38197-3_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38196-6
Online ISBN: 978-3-642-38197-3
eBook Packages: Computer ScienceComputer Science (R0)