Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs

About this paperEnglish中文日本語beside Englishbeside 中文beside 日本語

This paper is under a licence that does not allow it to be reproduced, so what is here is its front matter and a short abstract. Read it at the publisher's page.

Có thể giải phóng lập trình khỏi phong cách von Neumann? Một phong cách hàm và đại số của các chương trình

John Backus

Phòng thí nghiệm Nghiên cứu IBM, San Jose

Các ngôn ngữ lập trình truyền thống ngày càng trở nên khổng lồ hơn, nhưng không mạnh hơn. Những khiếm khuyết cố hữu ở mức cơ bản nhất khiến chúng vừa cồng kềnh vừa yếu: phong cách lập trình nguyên thủy theo từng từ một của chúng được thừa hưởng từ tổ tiên chung là máy tính von Neumann, sự gắn kết chặt chẽ của ngữ nghĩa với các chuyển đổi trạng thái, sự phân chia lập trình thành một thế giới của các biểu thức và một thế giới của các câu lệnh, sự bất lực của chúng trong việc sử dụng hiệu quả các dạng kết hợp mạnh để xây dựng các chương trình mới từ những chương trình hiện có, và sự thiếu vắng các tính chất toán học hữu ích để suy luận về các chương trình.

Một phong cách lập trình hàm thay thế được xây dựng dựa trên việc sử dụng các dạng kết hợp để tạo ra các chương trình. Các chương trình hàm xử lý dữ liệu có cấu trúc, thường không lặp lại và không đệ quy, được xây dựng theo thứ bậc, không đặt tên cho các đối số của chúng, và không yêu cầu cơ chế phức tạp của các khai báo thủ tục để trở nên có khả năng áp dụng tổng quát. Các dạng kết hợp có thể sử dụng các chương trình cấp cao để xây dựng những chương trình còn ở cấp cao hơn theo một phong cách không thể có trong các ngôn ngữ truyền thống.

Gắn với phong cách lập trình hàm là một đại số của các chương trình, trong đó các biến của nó lấy giá trị trên các chương trình và các phép toán của nó là các dạng kết hợp. Đại số này có thể được sử dụng để biến đổi các chương trình và giải các phương trình mà các “ẩn số” là các chương trình theo cách rất giống với việc người ta biến đổi các phương trình trong đại số trung học.

References

  1. Arvind, and Gostelow, K.P. A new interpreter for data flow schemas and its implications for computer architecture. Tech. Rep. No. 72, Dept. Comptr. Sci., U. of California, Irvine, Oct. 1975.
  2. Backus, J. Programming language semantics and closed applicative languages. Conf. Record ACM Symp. on Principles of Programming Languages, Boston, Oct. 1973, 71–86.
  3. Berkling, K.J. Reduction languages for reduction machines. Interner Bericht ISF-76-8, Gesellschaft für Mathematik und Datenverarbeitung MBH, Bonn, Sept. 1976.
  4. Burge, W.H. Recursive Programming Techniques. Addison-Wesley, Reading, Mass., 1975.
  5. Church, A. The Calculi of Lambda-Conversion. Princeton U. Press, Princeton, N.J., 1941.
  6. Curry, H.B., and Feys, R. Combinatory Logic, Vol. 1. North-Holland Pub. Co., Amsterdam, 1958.
  7. Dennis, J.B. First version of a data flow procedure language. Tech. Mem. No. 61, Lab. for Comptr. Sci., M.I.T., Cambridge, Mass., May 1973.
  8. Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.
  9. Friedman, D.P., and Wise, D.S. CONS should not evaluate its arguments. In Automata, Languages and Programming, S. Michaelson and R. Milner, Eds., Edinburgh U. Press, Edinburgh, 1976, pp. 257–284.
  10. Henderson, P., and Morris, J.H. Jr. A lazy evaluator. Conf. Record Third ACM Symp. on Principles of Programming Languages, Atlanta, Ga., Jan. 1976, pp. 95–103.
  11. Hoare, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), 576–583. Read it here
  12. Iverson, K. A Programming Language. Wiley, New York, 1962.
  13. Kosinski, P. A data flow programming language. Rep. RC 4264, IBM T.J. Watson Research Ctr., Yorktown Heights, N.Y., March 1973.
  14. Landin, P.J. The mechanical evaluation of expressions. Computer J. 6, 4 (1964), 308–320.
  15. Magó, G.A. A network of microprocessors to execute reduction languages. To appear in Int. J. Comptr. and Inform. Sci.
  16. Manna, Z., Ness, S., and Vuillemin, J. Inductive methods for proving properties of programs. Comm. ACM 16, 8 (Aug. 1973) 491–502.
  17. McCarthy, J. Recursive functions of symbolic expressions and their computation by machine, Pt. 1. Comm. ACM 3, 4 (April 1960), 184–195.
  18. McJones, P. A Church-Rosser property of closed applicative languages. Rep. RJ 1589, IBM Res. Lab., San Jose, Calif., May 1975.
  19. Reynolds, J.C. GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept. Comm. ACM 13, 5 (May 1970), 308–318.
  20. Reynolds, J.C. Notes on a lattice-theoretic approach to the theory of computation. Dept. Syst. and Inform. Sci., Syracuse U., Syracuse, N.Y., 1972.
  21. Scott, D. Outline of a mathematical theory of computation. Proc. 4th Princeton Conf. on Inform. Sci. and Syst., 1970.
  22. Scott, D. Lattice-theoretic models for various type-free calculi. Proc. Fourth Int. Congress for Logic, Methodology, and the Philosophy of Science, Bucharest, 1972.
  23. Scott, D., and Strachey, C. Towards a mathematical semantics for computer languages. Proc. Symp. on Comptrs. and Automata, Polytechnic Inst. of Brooklyn, 1971.

Read off the page by a vision model reading the page images using olmOCR-2-7B-1025-FP8. Translated into Tiếng Việt by gpt-5, against glossary version 7. Translated from the English.