Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-25T08:58:49.320Z Has data issue: false hasContentIssue false
  • English
  • Français

A consistent semantics of self-adjusting computation

Part of: JFP Research Articles

Published online by Cambridge University Press:  22 October 2013

UMUT A. ACAR ,
MATTHIAS BLUME  and
JACOB DONHAM
UMUT A. ACAR
Affiliation:
Carnegie Mellon University, Pittsburgh, PA 15213, USA (e-mail: [email protected])
MATTHIAS BLUME
Affiliation:
Google Inc., Chicago, IL, USA (e-mail: [email protected])
JACOB DONHAM
Affiliation:
Twitter Inc., San Francisco, CA, USA (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

This paper presents a semantics of self-adjusting computation and proves that the semantics is correct and consistent. The semantics introduces memoizing change propagation, which enhances change propagation with the classic idea of memoization to enable reuse of computations even when memory is mutated via side effects. During evaluation, computation reuse via memoization triggers a change-propagation algorithm that adapts the reused computation to the memory mutations (side effects) that took place since the creation of the computation. Since the semantics includes both memoization and change propagation, it involves both non-determinism (due to memoization) and mutation (due to change propagation). Our consistency theorem states that the non-determinism is not harmful: any two evaluations of the same program starting at the same state yield the same result. Our correctness theorem states that mutation is not harmful: Self-adjusting programs are compatible with purely functional programming. We formalize the semantics and its meta-theory in the LF logical framework and machine check our proofs using Twelf.

Type
Articles
Information
Journal of Functional Programming , Volume 23 , Issue 3 , May 2013 , pp. 249 - 292
Copyright
Copyright © Cambridge University Press 2013 

References

Abadi, M., Lampson, B. W. & Lévy, J.-J. (1996) Analysis and caching of dependencies. In International Conference on Functional Programming, pp. 83–91.CrossRefGoogle Scholar
Acar, U. A. (May 2005) Self-Adjusting Computation. PhD thesis, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA.Google Scholar
Acar, U. A., Ahmed, A. & Blume, M. (2008) Imperative self-adjusting computation. In Proceedings of the 25th Annual ACM Symposium on Principles of Programming Languages.CrossRefGoogle Scholar
Acar, U. A., Blelloch, G. E., Blume, M., Harper, R. & Tangwongsan, K. (2009) An experimental analysis of self-adjusting computation. ACM Trans. Prog. Lang. Sys. 32 (1), 31–53.CrossRefGoogle Scholar
Acar, U. A., Blelloch, G. E. & Harper, R. (2003) Selective memoization. In Proceedings of the 30th Annual ACM Symposium on Principles of Programming Languages.CrossRefGoogle Scholar
Acar, U. A., Blelloch, G. E. & Harper, R. (2006) Adaptive functional programming. ACM Trans. Prog. Lang. Sys. 28 (6), 990–1034.CrossRefGoogle Scholar
Acar, U. A., Blelloch, G. E., Harper, R., Vittes, J. L. & Woo, M. (2004) Dynamizing static algorithms with applications to dynamic trees and history independence. In ACM-SIAM Symposium on Discrete Algorithms, pp. 531–540.Google Scholar
Acar, U. A., Blume, M. & Donham, J. (2007) A consistent semantics of self-adjusting computation. In European Symposium on Programming.CrossRefGoogle Scholar
Acar, U. A., Cotter, A., Hudson, B. & Türkoğlu, D. (2010) Dynamic well-spaced point sets. In Symposium on Computational Geometry.CrossRefGoogle Scholar
Alstrup, S., Holm, J., de Lichtenberg, K. & Thorup, M. (1997) Minimizing diameters of dynamic trees. In Automata, Languages and Programming, Degano, P., Gorrieri, R. & Marchetti-Spaccamela, A. (eds.), pp. 270–280.CrossRefGoogle Scholar
Bellman, R. (1957) Dynamic Programming. Princeton University Press.Google ScholarPubMed
Bhatotia, P., Wieder, A., Rodrigues, R., Acar, U. A., & Pasquini, R. (2011) Incoop: MapReduce for incremental computations. In ACM Symposium on Cloud Computing.CrossRefGoogle Scholar
Brodal, G. S. & Jacob, R. (2002) Dynamic planar convex hull. In Proceedings of the 43rd Annual IEEE Symposium on Foundations of Computer Science, pp 617–626.CrossRefGoogle Scholar
Burckhardt, S., Leijen, D., Sadowski, C., Yi, J. & Ball, T. (2011) Two for the price of one: A model for parallel and incremental computation. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications.CrossRefGoogle Scholar
Carlsson, M. (2002) Monads for incremental computing. In International Conference on Functional Programming, pp. 26–35.CrossRefGoogle Scholar
Chiang, Y.-J. & Tamassia, R. (1992) Dynamic algorithms in computational geometry. Proc. IEEE 80 (9), 1412–1434.CrossRefGoogle Scholar
Cohen, R. F. & Tamassia, R. (1991) Dynamic expression trees and their applications. In Proceedings of the 2nd Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 52–61.Google Scholar
Cooper, G. H. & Krishnamurthi, S. (April 2004) FrTime: Functional Reactive Programming in PLT Scheme. Technical Report CS-03-20, Department of Computer Science, Brown University, Providence, RI.Google Scholar
Cooper, G. H. & Krishnamurthi, S. (2006) Embedding dynamic dataflow in a call-by-value language. In Proceedings of the 15th Annual European Symposium on Programming (ESOP).CrossRefGoogle Scholar
Demers, A., Reps, T. & Teitelbaum, T. (1981) Incremental evaluation of attribute grammars with application to syntax-directed editors. In Symposium on Principles of Programming Languages, pp. 105–116.CrossRefGoogle Scholar
Demetrescu, C., Finocchi, I., & Italiano, G. F. (2005a) Dynamic graphs. In Handbook on Data Structures and Applications, Chap. 36: Boca Raton, FL: CRC Press.Google Scholar
Demetrescu, C., Finocchi, I. & Italiano, G. F. (2005b) Dynamic Trees. In Handbook on Data Structures and Applications. Mehta, D. & Sahni, S. (eds), Chap. 35, CRC Press Series in Computer and Information Science. Boca Raton, FL: CRC Press.Google Scholar
Elliott, C. (1998) Functional implementations of continuous modeled animation. Lect Notes Comput. Sci. 1490, 284–299.CrossRefGoogle Scholar
Elliott, C. & Hudak, P. (1997) Functional reactive animation. In Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming. Rochester, NY: ACM, pp. 263–273.CrossRefGoogle Scholar
Eppstein, D., Galil, Z. & Italiano, G. F. (1999) Dynamic graph algorithms. In Algorithms and Theory of Computation Handbook, Atallah, M. J. (ed), Chap. 8. Boca Raton, FL: CRC Press.Google Scholar
Eppstein, D., Galil, Z., Italiano, G. F., & Nissenzweig, A. (1997) Sparsification – a technique for speeding up dynamic graph algorithms. J. ACM 44 (5), 669–696.CrossRefGoogle Scholar
Field, J. (November 1991) Incremental Reduction in the Lambda Calculus and Related Reduction Systems. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY.CrossRefGoogle Scholar
Field, J. & Teitelbaum, T. (1990) Incremental reduction in the lambda calculus. In ACM Conference LISP and Functional Programming, pp. 307–322.CrossRefGoogle Scholar
Frederickson, G. N. (1985) Data structures for on-line updating of minimum spanning trees, with applications. SIAM J. Comput. 14, 781–798.CrossRefGoogle Scholar
Frederickson, G. N. (1997) A data structure for dynamically maintaining rooted trees. J. Algorithms 24 (1), 37–65.CrossRefGoogle Scholar
Graham, R. L. (1972) An efficient algorithm for determining the convex hull of a finete planar set. Inf. Process. Lett. 1, 132–133.CrossRefGoogle Scholar
Guibas, L. (2004) Modeling motion. In Handbook of Discrete and Computational Geometry, Goodman, J. & O'Rourke, J. (eds.), 2nd ed. Boca Raton, FL: Chapman and Hall/CRC Press, pp. 1117–1134.Google Scholar
Hammer, M. A., Acar, U. A. & Chen, Y. (2009) CEAL: A C-based language for self-adjusting computation. In ACM SIGPLAN Conference on Programming Language Design and Implementation.CrossRefGoogle Scholar
Hammer, M., Acar, U. A., Rajagopalan, M. & Ghuloum, A. (2007) A proposal for parallel self-adjusting computation. In DAMP '07: Workshop on Declarative Aspects of Multicore Programming.CrossRefGoogle Scholar
Hammer, M., Neis, G., Chen, Y. & Acar, U. A. (2011) Self-adjusting stack machines. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).CrossRefGoogle Scholar
Harper, R., Honsell, F. & Plotkin, G. (January 1993) A framework for defining logics. J. Assoc. Comput. Mach. 40 (1),143–184.CrossRefGoogle Scholar
Harper, R. & Licata, D. R. (2007) Mechanizing metatheory in a logical framework. J. Funct. Program. 17 (4–5), 613–673.CrossRefGoogle Scholar
Hedin, G. (March 1992) Incremental Semantics Analysis. PhD thesis, Department of Computer Science, Lund University, Lund, Sweden.Google Scholar
Henzinger, M. R. & King, V (1997) Maintaining minimum spanning trees in dynamic graphs. In ICALP '97: Proceedings of the 24th International Colloquium on Automata, Languages and Programming. Berlin, Germany: Springer-Verlag, pp. 594–604.Google Scholar
Henzinger, M. R. & King, V. (1999) Randomized fully dynamic graph algorithms with polylogarithmic time per operation. J. ACM 46 (4), 502–516.CrossRefGoogle Scholar
Heydon, A., Levin, R. & Yu, Y. (2000) Caching function calls using precise dependencies. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 311–320.CrossRefGoogle Scholar
Holm, J., de Lichtenberg, K. & Thorup, M. (2001) Poly-logarithmic deterministic fully dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity. J. ACM 48 (4), 723–760.CrossRefGoogle Scholar
Hoover, R. (May 1987) Incremental Graph Evaluation. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY.Google Scholar
Ley-Wild, R., Acar, U. A., & Fluet, M. (July 2008a) A Cost Semantics for Self-Adjusting Computation. Technical Report CMU-CS-08-141, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA.Google Scholar
Ley-Wild, R., Acar, U. A. & Fluet, M. (2009) A cost semantics for self-adjusting computation. In Proceedings of the 26th Annual ACM Symposium on Principles of Programming Languages.CrossRefGoogle Scholar
Ley-Wild, R., Fluet, M. & Acar, U. A. (2008b) Compiling self-adjusting programs with continuations. In International Conference on Functional Programming, Victoria, British Columbia, Canada.Google Scholar
Liu, Y. A., Stoller, S. & Teitelbaum, T. (1998) Static caching for incremental computation. ACM Trans. Program. Lang. Syst. 20 (3), 546–585.CrossRefGoogle Scholar
McCarthy, J. (1963) A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, Braffort, P. & Hirschberg, D. (eds), Amsterdam, Netherlands: North-Holland, pp. 33–70.CrossRefGoogle Scholar
Michie, D. (1968) “Memo” functions and machine learning. Nature 218, 19–22.CrossRefGoogle Scholar
Overmars, M. H. & van Leeuwen, J. (1981) Maintenance of configurations in the plane. J. Comput. Syst. Sci. 23, 166–204.CrossRefGoogle Scholar
Pfenning, F. & Schürmann, C. (July 1999) System description: Twelf – A meta-logical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16), Trento, Italy, Ganzinger, H. (ed),. LNAI 1632. Berlin, Germany: Springer-Verlag, pp. 202–206.CrossRefGoogle Scholar
Pugh, W. & Teitelbaum, T. (1989) Incremental computation via function caching. In 16th Symposium on Principles of Programming Languages, pp. 315–328. New York, NY: ACM.Google Scholar
Ramalingam, G. & Reps, T. (1993) A categorized bibliography on incremental computation. In Proceedings of the 20th Symposium on Principles of Programming Languages, pp. 502–510.CrossRefGoogle Scholar
Reps, T. (August 1982a) Generating Language-Based Environments. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY.Google Scholar
Reps, T. (1982b) Optimal-time incremental semantic analysis for syntax-directed editors. In Proceedings of the 9th Annual Symposium on Principles of Programming Languages, pp. 169–176.CrossRefGoogle Scholar
Shankar, A. & Bodik, R. (2007) DITTO: Automatic incrementalization of data structure invariant checks (in Java). In International Conference on Programming Language Design and Implementation (PLDI).CrossRefGoogle Scholar
Sleator, D. D. & Tarjan, R. E. (1983) A data structure for dynamic trees. J. Comput. Syst. Sci. 26 (3), 362–391.CrossRefGoogle Scholar
Sleator, D. D. and Tarjan, R. E. (1985) Self-adjusting binary search trees. J. ACM 32 (3), 652–686.CrossRefGoogle Scholar
Sümer, Ö., Acar, U. A., Ihler, A. & Mettu, R. (2011) Adaptive exact inference in graphical models. J. Mach. Learn. 8, 180–186.Google Scholar
Sundaresh, R. S. & Hudak, P. (1991) Incremental compilation via partial evaluation. In Conference Record of the 18th Annual ACM Symposium on Principles of Programming Languages, pp. 1–13.Google Scholar
Tarjan, R. & Werneck, R. (2007) Dynamic trees in practice. In Proceedings of the 6th Workshop on Experimental Algorithms (WEA 2007), pp. 80–93.CrossRefGoogle Scholar
Wan, Z. & Hudak, P. (2000) Functional reactive programming from first principles. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation. New York, NY: ACM, pp. 242–252.CrossRefGoogle Scholar
Wan, Z., Taha, W., & Hudak, P. (2001) Real-time FRP. SIGPLAN Not. 36 (10), 146–156.CrossRefGoogle Scholar
Yellin, D. M. & Strom, R. E. (April 1991) INC: A language for incremental computations. ACM Trans. Program. Lang. Syst. 13 (2), 211–236.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.