zbMATH — the first resource for mathematics

Limited second-order functionality in a first-order setting. (English) Zbl 1468.68291
Summary: We describe how we have defined in ACL2 a weak version of the Common Lisp functional apply, which takes a function and list of actuals and applies the function to the actuals. Our version, called apply$, does not operate on functions but on ordinary objects – symbols and lists representing lambda expressions – some of which are interpreted as functions. We define a syntactic notion of “tameness” to identify the interpretable objects. This makes our apply$ weaker than a true second-order functional but we believe apply$ is powerful enough for many uses in ACL2. To maintain soundness and the conservativity of our Definitional Principle we require that certain hypotheses, called “warrants”, be present in any theorem relying on the behavior of apply$ on non-primitives. Within these constraints we can define “functionals” such as sum and foldr which map tame “functions” over lists and accumulate the results. This allows the ACL2 user to avoid defining specialized recursive functions for each such application. We can prove and use general-purpose lemmas about these “functionals.” We describe the formalization, explain how we keep the Definitional Principle conservative, show examples of useful functions using apply$ and theorems about them, sketch the proof that there is a model of any extension of the system using the new primitives, discuss issues arising in making these functions executable, and show some preliminary performance results.
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
68N15 Theory of programming languages
68N18 Functional programming and lambda calculus
Full Text: DOI
[1] Andrews, Pb; Brown, Ce, TPS: a hybrid automatic-interactive system for developing proofs, J. Appl. Log., 4, 4, 367-395 (2006) · Zbl 1107.68091
[2] Beeson, M.: Otter-lambda, a theorem-prover with untyped lambda-unification. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proceedings of the ESFOR Workshop at IJCAR 2004 (2004)
[3] Benzmüller, C.; Sultana, N.; Paulson, Lc; Theiß, F., The higher-order prover LEO-II, J. Autom. Reason., 55, 4, 389-404 (2015) · Zbl 1356.68176
[4] Bertot, Y.; Castran, P., Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (2010), Berlin: Springer, Berlin
[5] Blanchette, Jc; Kaliszyk, C.; Paulson, Lc; Urban, J., Hammering towards QED, J. Formaliz. Reason., 9, 1, 101-148 (2016) · Zbl 1451.68318
[6] Boyer, R.; Moore, Js, The addition of bounded quantification and partial functions to a computational logic and its theorem prover, J. Autom. Reason., 4, 2, 117-172 (1988) · Zbl 0653.03007
[7] Boyer, Rs; Moore, Js, A Computational Logic Handbook (1997), New York: Academic Press, New York
[8] Boyer, Rs; Goldschlag, Dm; Kaufmann, M.; Moore, Js; Lifschitz, V., Functional instantiation in first-order logic, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, 7-26 (1991), London: Academic Press, London · Zbl 0755.68120
[9] Brock, B.; Kaufmann, M.; Moore, Js, Rewriting with equivalence relations in ACL2, J. Autom. Reason., 40, 4, 293-306 (2008) · Zbl 1140.68029
[10] Brown, C.E.: Satallax: an automatic higher-order prover. In: Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, 26-29 June 2012. Proceedings, pp. 111-117 (2012) · Zbl 1358.68250
[11] Chamarthi, Harsh Raju; Dillinger, Peter C.; Manolios, Panagiotis, Data Definitions in the ACL2 Sedan, Electronic Proceedings in Theoretical Computer Science, 152, 27-48 (2014)
[12] Goel, S., Hunt, W.A., Kaufmann, M.: Simulation and formal verification of x86 machine-code programs that make system calls. In: Claessen, K., Kuncak, V. (eds.) FMCAD’14: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, pp. 91-98. EPFL, Switzerland (2014)
[13] Goel, S.: Formal verification of application and system programs based on a validated x86 ISA model. Ph.D. thesis, University of Texas at Austin (2016)
[14] Gordon, Mjc, On the power of list iteration, Comput. J., 22, 4, 376-379 (1979) · Zbl 0425.68015
[15] Gordon, Mjc; Melham, Tf, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic (1993), New York: Cambridge University Press, New York
[16] Greve, D.; Kaufmann, M.; Manolios, P.; Moore, Js; Ray, S.; Ruiz-Reina, Jl; Sumners, R.; Vroon, D.; Wilding, M., Efficient execution in an automated reasoning environment, J. Funct. Program., 18, 1, 15-46 (2008) · Zbl 1128.68090
[17] Hunt, Warren A.; Kaufmann, Matt; Moore, J. Strother; Slobodova, Anna, Industrial hardware and software verification with ACL2, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375, 2104, 20150399 (2017)
[18] Kaufmann, M.: Trusted extension of ACL2 system code: towards an open architecture. In: Workshop on Trusted Extensions of Interactive Theorem Provers (2010). See https://urldefense.proofpoint.com/v2/url?u=http-3A__www.cs.utexas.edu_users_=DwIBAg=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E=NXMiBg4nq_C3pnEnk6Tdql75ei8JA-JX02usDOKVdmM=kaufmann/itp-trusted-extensions-aug-2010/. Accessed 2018
[19] Kaufmann, M.; Manolios, P.; Moore, Js, Computer-Aided Reasoning: An Approach (2000), Boston: Kluwer Academic Press, Boston
[20] Kaufmann, M., Moore, J.S.: The ACL2 home page. In: Department of Computer Sciences, University of Texas at Austin (2018). https://urldefense.proofpoint.com/v2/url?u=http-3A__www.cs.utexas.edu_users_moore_acl2_=DwIBAg=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E=gWfwZpi-faeBogx3pJCo6I5MQjZlJlpVPXbBI0MGPUQ=. Accessed 2018
[21] Kaufmann, M., Moore, J.S.: ACL2 User Community: ACL2 sources and ACL2 community books on GitHub. In: GitHub (2018). https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_acl2_acl2=DwIBAg=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E=NrpdCC6fmnRh_I8oVVLD24qw6YElaOcVQiS7xqUk3eg=. Accessed 2018
[22] Kunčar, O.: Correctness of Isabelle’s cyclicity checker: implementability of overloading in proof assistants. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP ’15, pp. 85-94, New York, NY, USA. ACM (2015)
[23] Mccarthy, J., Recursive functions of symbolic expressions and their computation by machine (part I), CACM, 3, 4, 184-195 (1960) · Zbl 0101.10413
[24] McCune, W.: Otter 3.0 reference manual and guide. Technical report ANL-94/6, Argonne National Laboratory, Argonne, IL (1994). See also https://urldefense.proofpoint.com/v2/url?u=http-3A__www.mcs.anl.gov_AR_otter_=DwIBAg=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E=bQ9nItKqAZKGDoFo__COKKQuPtL-9Qhqa7CZa4HLPgg=. Accessed 2018
[25] Meng, J.; Paulson, Lc, Translating higher-order clauses to first-order clauses, J. Autom. Reason., 40, 1, 35-60 (2008) · Zbl 1203.68188
[26] Meseguer, J., Twenty years of rewriting logic, J. Log. Algebr. Program., 81, 7, 721-781 (2012) · Zbl 1267.03043
[27] Paulson, Lc, ML for the Working Programmer (1991), New York: Cambridge University Press, New York
[28] Paulson, Lc, Isabelle: A Generic Theorem Prover. LNCS 828 (1994), Berlin: Springer, Berlin · Zbl 0825.68059
[29] Pitman, K.: The common lisp HyperSpec. See https://urldefense.proofpoint.com/v2/url?u=http-3A__www.lispworks.com_documentation_common-2Dlisp=DwIBAg=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E=_Wd_KHgA45uc-8RythKrUZF9qgc-wNTUA3k7JyZh1zE=.html. Accessed 2018
[30] Reynolds, Jc, Definitional interpreters for higher-order programming languages, High. Order Symbol. Comput., 11, 4, 363-397 (1998) · Zbl 0934.68034
[31] Steele, Gl Jr, Common Lisp the Language (1990), Burlington: Digital Press, Burlington · Zbl 0757.68008
[32] The Haskell home page. https://urldefense.proofpoint.com/v2/url?u=https-3A__www.haskell.org=DwIBAg=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E=MIT0gLXrGfuoJ3pMHEAFlrqshodFFiClh_eQ8wpP7FA=. Accessed 2018
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.