×

Prelogical relations. (English) Zbl 1012.03039

Summary: We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful as well as further algebraic properties including composability. The basic idea is simply to require the reverse implication in the definition of logical relations to hold only for pairs of functions that are expressible by the same lambda term. Prelogical relations are the minimal weakening of logical relations that gives composability for extensional structures and simultaneously the most liberal definition that gives the Basic Lemma. Prelogical predicates (i.e., unary prelogical relations) coincide with sets that are invariant under Kripke logical relations with varying arity as introduced by Jung and Tiuryn, and prelogical relations are the closure under projection and intersection of logical relations. These conceptually independent characterizations of prelogical relations suggest that the concept is rather intrinsic and robust. The use of prelogical relations gives an improved version of Mitchell’s representation independence theorem which characterizes observational equivalence for all signatures rather than just for first-order signatures. Prelogical relations can be used in place of logical relations to give an account of data refinement where the fact that prelogical relations compose explains why stepwise refinement is sound.

MSC:

03B70 Logic in computer science
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S.: Abstract interpretation, logical relations, and kan extensions. J. logic comput. 1, 5-40 (1990) · Zbl 0727.03020
[2] Alimohamed, M.: A characterization of lambda definability in categorical models of implicit polymorphism. Theoret. comput. Sci. 146, 5-23 (1995) · Zbl 0873.68015
[3] Altenkirch, T.1998, Logical relations and inductive/coinductive types, inProc. Computer Science Logic, CSL’98, Brno, Lecture Notes in Computer Science, Vol. 1584, pp. 343–354, Springer-Verlag, Berlin.
[4] Curien, P.-L.1993, Categorical Combinators, Sequential Algorithms, and Functional Programming, 2nd ed., Birkhäuser, Basel. · Zbl 0814.68085
[5] Di Gianantonio, P., and Honsell, F.1993, An abstract notion of application, inProc. Intl. Conf. on Typed Lambda Calculi and Applications, Utrecht, Lecture Notes in Computer Science, Vol. 664, pp. 124–138, Springer-Verlag, Berlin. · Zbl 0788.68090
[6] Gandy, R.1980, Proofs of strong normalization, inTo H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 457–477, Academic Press, San Diego.
[7] Ginzburg, A. 1968, Algebraic Theory of Automata, Academic Press, San Diego. · Zbl 0195.02501
[8] Honsell, F., Longley, J., Sannella, D., and Tarlecki, A.2000, Constructive data refinement in typed lambda calculus, inProc. 2nd Intl. Conf. on Foundations of Software Science and Computation Structures, European Joint Conferences on Theory and Practice of Software (ETAPS’2000), Berlin, Lecture Notes in Computer Science, Vol. 1784, pp. 149–164, Springer-Verlag, Berlin. · Zbl 0965.68012
[9] Honsell, F., and Sannella, D.1999, Pre-logical relations, inProc. Computer Science Logic, CSL’99, Madrid, Lecture Notes in Computer Science, Vol. 1683, pp. 546–561, Springer-Verlag, Berlin. · Zbl 0942.03018
[10] Jung, A., and Tiuryn, J.1993, A new characterization of lambda definability, inProc. Intl. Conf. on Typed Lambda Calculi and Applications, Utrecht, Lecture Notes in Computer Science, Vol. 664, pp. 245–257, Springer-Verlag, Berlin. · Zbl 0795.03021
[11] Kinoshita, Y., O’Hearn, P., Power, J., Takeyama, M., and Tennent, R.1997, An axiomatic approach to binary logical relations with applications to data refinement, inProc. TACS’97, Lecture Notes in Computer Science, Vol. 1281, pp. 191–212, Springer-Verlag, Berlin. · Zbl 0882.18006
[12] Loader, R. 2001, The undecidability of {\(\lambda\)}-definability, in, Logic, Meaning and Computation: Essays in Memory of Alonzo Church, Kluwer Academic, Dordrecht/Norwell, MA.
[13] Longley, J.: Matching typed and untyped realizability. Electronic notes in theor. Comput. sci. 23 (1999) · Zbl 0958.68096
[14] Ma, Q., and Reynolds, J.1992, Types, abstraction, and parametric polymorphism, part 2, inProc. 7th Intl. Conf. on Mathematical Foundations of Programming Semantics, Pittsburgh, Lecture Notes in Computer Science, Vol. 598, pp. 1–40, Springer-Verlag, Berlin.
[15] Marz, M, Rohr, A, and, Streicher, T. 1999, Full abstraction and universality via realisability, in, Proc. 14th IEEE Symp. on Logic in Computer Science, Trento.
[16] Milner, R.1971, An algebraic definition of simulation between programs, inProc. 2nd Intl. Joint Conf. on Artificial Intelligence, pp. 481–489, British Computer Society.
[17] Mitchell, J. 1990, Type systems for programming languages, in, Handbook of Theoretical Computer Science, Vol, B, Chap. 8, Elsevier, Amsterdam.
[18] Mitchell, J.1991, On the equivalence of data representations, inArtificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthyV. Lifschitz, Ed., pp. 305–330, Academic Press, San Diego.
[19] Mitchell, J. 1996, Foundations for Programming Languages, MIT Press, Cambridge, MA.
[20] Mitchell, J., and Meyer, A.1985, Second-order logical relations, inProc. of the Conf. on Logic of Programs, Brooklyn, Lecture Notes in Computer Science, Vol, 193, pp. 225–236, Springer-Verlag, Berlin.
[21] Mitchell, J.; Moggi, E.: Kripke-style models for typed lambda calculus. Ann. pure appl. Logic 51, 99-124 (1991) · Zbl 0728.03011
[22] O’hearn, P.; Riecke, J.: Kripke logical relations and PCF. Inform. and comput. 120, 107-116 (1995) · Zbl 0912.03008
[23] Plotkin, G.1980, Lambda-definability in the full type hierarchy, inTo H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 363–373, Academic Press, San Diego.
[24] Plotkin, G., Power, J., Sannella, D., and Tennent, R.2000, Lax logical relations, inProc. 27th Intl. Colloq. on Automata, Languages and Programming, Geneva, Lecture Notes in Computer Science, Vol. 1853, pp. 85–102, Springer-Verlag, Berlin. · Zbl 0973.03016
[25] Power, J, and, Robinson, E. 2000, Logical relations and data abstraction, in, Proc. Computer Science Logic, CSL 2000, Fischbachau, Lecture Notes in Computer Science, Vol, 1862, Springer-Verlag, Berlin. · Zbl 0973.68148
[26] Power, J, and, Robinson, E. 2000, Logical relations, data abstraction and structured fibrations, in, Proc. 2nd Intl. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming, Montreal. · Zbl 0973.68148
[27] Riecke, J.; Sandholm, A.: A relational account of call-by-value sequentiality. Inform. and comput., 258-267 (1997) · Zbl 1096.68019
[28] Robinson, E. 1996, Logical relations and Data Abstraction, Report 730, Queen Mary and Westfield College. · Zbl 0973.68148
[29] Sannella, D.; Tarlecki, A.: On observational equivalence and algebraic specifications. J. comput. System sci. 34, 150-178 (1987) · Zbl 0619.68028
[30] Sannella, D.; Tarlecki, A.: Toward formal development of programs from algebraic specifications: implementations revisited. Acta inform. 25, 233-281 (1988) · Zbl 0621.68004
[31] Schoett, O. 1987, Data Abstraction and the Correctness of Modular Programming, Ph.D. thesis CST-42-87, Univ. of Edinburgh.
[32] Statman, R.: {\(\lambda\)}-definable functionals and \({\beta}{\eta}\) conversion. Arch. math. Logik 23, 21-26 (1983) · Zbl 0537.03009
[33] Statman, R.: Logical relations and the typed lambda calculus. Inform. and control 65, 85-97 (1985) · Zbl 0594.03006
[34] Tennent, R. 1994, Correctness of data representations in Algol-like languages, in, A Classical Mind: Essays in Honour of C.A.R. Hoare, Prentice Hall, New York.
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.