Survey: A survey of state vectors
Abstract
The theory of Turing machines, which is basic to proving the various limitations of computers, is quite well known. The theory of finite state automata, the basic hardware models such as Moore machines, Mealy machines, and their generalizations, are similarly well known. Our purpose here is to survey basic work done between 1958 and 1975 on still another mathematical model for computer science, the state vector model. In this model there are many variables, each with its own current value, rather than a single state; this makes the model closer to what happens in a real computer.
References
[1]
Aho, A.V. and Ullman, J.D., Optimization of straight line programs. SIAM Journal on Computing. v1 i1. 1-19.
[2]
Allen, F.E., Program optimization. Annual Review in Automatic Programming. v5. 239-307.
[3]
Parsing algorithms with backtrack. Information and Control. v23 i1. 1-34.
[4]
Flowchart machines. BIT. v10 i4. 415-442.
[5]
Böhm, C. and Jacopini, G., Flow diagrams, Turing machines, and languages with only two formation rules. Communications of the ACM. v9 i5. 366-371.
[6]
Burstall, R.M., Semantics of assignment. Machine Intelligence. v2. 3-20.
[7]
Burstall, R.M., Proving properties of programs by structural induction. Computer Journal. v12 i1. 41-48.
[8]
Burstall, R.M., Formal description of program structure and semantics in first-order logic. Machine Intelligence. v5. 79-98.
[9]
R.M. Burstall, An algebraic description of programs with assertions, verification, and simulation, in: Proc. ACM Conf. on Proving Assertions about Programs (SIGPLAN Notices 7(1); SIGACT News 14), 1972, pp. 7-14
[10]
Burstall, R.M., Some techniques for proving correctness of programs which alter data structures. Machine Intelligence. v7. 23-50.
[11]
Church, A., The Calculi of Lambda-Conversion. 1941. Oxford University Press.
[12]
Constable, R.L. and Borodin, A.B., Subrecursive programming languages, part I: Efficiency and program structure. Journal of the ACM. v19 i3. 526-568.
[13]
Cook, S.A. and Reckhow, R.A., Time-bounded random access machines. Journal of Computer and System Sciences. v7. 354-375.
[14]
Cooper, D.C., Some transformations and standard forms of graphs, with applications to computer programs. Machine Intelligence. v2. 21-32.
[15]
Cooper, D.C., Program scheme equivalences and second-order logic. Machine Intelligence. v4. 3-15.
[16]
Curry, H.B., Foundations of Mathematical Logic. 1963. McGraw-Hill, New York.
[17]
Davis, M., Computability and Unsolvability. 1958. McGraw-Hill, New York.
[18]
de Bakker, J.W., Semantics of programming languages. In: Advances in Information Systems, vol. 2, Plenum Press, New York, London. pp. 173-227.
[19]
L.P. Deutsch, An interactive program verifier, Ph.D. Thesis, Department of Computer Science, University of California, Berkeley, 1973
[20]
Dijkstra, E.W., A constructive approach to the problem of program correctness. BIT. v8 i3. 174-186.
[21]
Ehlers, H., Logic by Way of Set Theory. 1968. Holt, Rinehart, and Winston, New York.
[22]
Elgot, C.C. and Robinson, A., Random-access stored program machines, an approach to programming languages. Journal of the ACM. v11 i4. 365-399.
[23]
Elgot, C.C., Abstract algorithms and diagram closure. In: Genuys, F. (Ed.), Programming Languages, Academic Press, London, New York. pp. 1-42.
[24]
Engeler, E., Algorithmic properties of structures. Mathematical Systems Theory. v1 i3. 183-195.
[25]
Ershov, A.P., Operator algorithms. I. Problems of Cybernetics. v3. 697-763.
[26]
Evans, A., An Algol 60 compiler. Annual Review in Automatic Programming. v4. 87-124.
[27]
Feldman, J.A., A formal semantics for computer languages and its application in a compiler-compiler. Communications of the ACM. v9 i1. 3-9.
[28]
Translator writing systems. Communications of the ACM. v11 i2. 77-113.
[29]
A descriptive language for symbol manipulation. Journal of the ACM. v8 i4. 579-584.
[30]
Floyd, R.W., On the nonexistence of a phrase-structure grammar for Algol 60. Communications of the ACM. v5 i9. 483-484.
[31]
Floyd, R.W., Assigning meanings to programs. In: Proc. Symp. Applied Math., Mathematical Aspects of Computer Science, vol. 19. American Mathematical Society, Providence, RI. pp. 19-32.
[32]
Garland, S.J. and Luckham, D.L., Program schemes, recursion schemes, and formal languages. Journal of Computer and Systems Sciences. v7 i2. 119-160.
[33]
Ginsburg, S., An Introduction to Mathematical Machine Theory. 1962. Addison-Wesley, Reading, Mass.
[34]
H.H. Goldstine, J. von Neumann, Planning and coding problems for an electronic computing instrument. Reprinted in The Collected Works of John von Neumann, vol. 5, Pergamon Press, 1963, pp. 80-235
[35]
D.I. Good, Toward a man-machine system for proving program correctness, Ph.D. Thesis, Computer Science Department, University of Wisconsin, 1970
[36]
Gries, D., Programming by induction. Information Processing Letters. v1 i3. 100-107.
[37]
Hartmanis, J., Computational complexity of random access stored program machines. Mathematical Systems Theory. v5 i3. 232-245.
[38]
Henderson, P., Derived semantics for some programming language constructs. Communications of the ACM. v15 i11. 967-973.
[39]
Hoare, C.A.R., An axiomatic basis for computer programming. Communications of the ACM. v12 i10. 576-580.
[40]
Hoare, C.A.R., Procedures and parameters: An axiomatic approach. In: Lecture Notes in Mathematics 188 (Semantics of Algorithmic Languages), Springer-Verlag, Berlin, Heidelberg, New York. pp. 102-116.
[41]
Igarashi, S., Semantics of Algol-like statements. In: Lecture Notes in Mathematics 188 (Semantics of Algorithmic Languages), Springer-Verlag, Berlin, Heidelberg, New York. pp. 117-177.
[42]
Kaluzhnin, L.A., Algorithmization of mathematical problems. Problems of Cybernetics. v2. 371-391.
[43]
Kaphengst, H., Eine abstrakte programmgesteuerte Rechenmaschine. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. v5. 366-379.
[44]
D.M. Kaplan, Correctness of a compiler for Algol-like programs, Artificial Intelligence Memorandum No. 48, Stanford University, 1967
[45]
Kaplan, D.M., Some completeness results in the mathematical theory of computation. Journal of the ACM. v15 i1. 124-134.
[46]
Kaplan, D.M., Regular expressions and the equivalence of programs. Journal of Computer and System Sciences. v3 i4. 361-386.
[47]
D.M. Kaplan, Recursion induction applied to generalized flowcharts, in: Proc. 24th National ACM Conference, 1969, pp. 491-504
[48]
Karp, R.M., A note on the application of graph theory to digital computer programming. Information and Control. v3 i2. 179-190.
[49]
J.C. King, A program verifier, Ph.D. Thesis, Department of Computer Science, Carnegie-Mellon University, 1969
[50]
King, J.C., Proving programs to be correct. IEEE Transactions on Computers. vC-20 i11. 1331-1336.
[51]
Knuth, D.E., Semantics of context-free languages. Mathematical Systems Theory. v2 i2. 127-145.
[52]
Knuth, D.E., . In: The Art of Computer Programming, vol. I: Fundamental Algorithms, Addison-Wesley, Reading, MA.
[53]
Knuth, D.E., Semantics of context-free languages - correction. Mathematical Systems Theory. v5 i1. 95-96.
[54]
Knuth, D.E., Examples of formal semantics. In: Lecture Notes in Mathematics 188 (Semantics of Algorithmic Languages), Springer-Verlag, Berlin, Heidelberg, New York. pp. 212-235.
[55]
Korolyuk, V.S., The concept of an addressed algorithm. Problems of Cybernetics. v4. 1241-1257.
[56]
Lambek, J., How to program an infinite abacus. Canadian Mathematical Bulletin. v4 i3. 295-302.
[57]
Landin, P.J., The mechanical evaluation of expressions. Computer Journal. v6 i4. 308-320.
[58]
Landin, P.J., A correspondence between Algol 60 and Church's lambda-notation. Communications of the ACM. v8. 89-101.
[59]
Landin, P.J., The next 700 programming languages. Communications of the ACM. v9 i3. 157-166.
[60]
P.J. Landin, A formal description of Algol 60, in: T.B. Steel Jr. (Ed.), Formal Language Description Languages for Computer Programming, North-Holland, Amsterdam, 1966, pp. 266-294
[61]
P. Lauer, Formal definition of Algol 60, Technical Report TR25.088, IBM Laboratory Vienna, 1968
[62]
P. Lauer, Consistent formal theories of the semantics of programming languages, Technical Report TR25.121, IBM Laboratory Vienna, 1971
[63]
Ledgard, H.F., A model for type checking: with an application to Algol 60. Communications of the ACM. v15 i11. 956-966.
[64]
Lee, J.A.N., The formal definition of the BASIC language. Computer Journal. v15 i1. 37-41.
[65]
London, R.L., Bibliography on proving the correctness of computer programs. Machine Intelligence. v5. 569-580.
[66]
London, R.L., Proving programs correct: Some techniques and examples. BIT. v10 i2. 168-182.
[67]
R.L. London, Correctness of a compiler for a Lisp subset, in: Proc. ACM Conf. on Proving Assertions about Programs (SIGPLAN Notices 7(1); SIGACT News 14), 1972, pp. 121-127
[68]
Lucas, P. and Walk, K., On the formal description of PL/I. Annual Review in Automatic Programming. v6 i3.
[69]
Luckham, D.C., Park, D.M.R. and Paterson, M.S., On formalised computer programs. Journal of Computer and System Sciences. v4 i3. 220-249.
[70]
Z. Manna, Termination of algorithms, Ph.D. Thesis, Department of Computer Science, Carnegie-Mellon University, 1968
[71]
Manna, Z., The correctness of programs. Journal of Computer and Systems Sciences. v3 i2. 119-127.
[72]
Z. Manna, Termination of programs represented as interpreted graphs, in: Proc. Spring Joint Computer Conf., 1970, pp. 83-89
[73]
Manna, Z. and Vuillemin, J., Fixpoint approach to the theory of computation. Communications of the ACM. v15 i7. 528-536.
[74]
Martin, D.F. and Estrin, G., Models of computations and systems - evaluation of vertex probabilities in graph models of computations. Journal of the ACM. v14 i2. 281-299.
[75]
Maurer, W.D., A theory of computer instructions. Journal of the ACM. v13 i2. 226-235.
[76]
Maurer, W.D., A semantic extension of BNF. International Journal of Computer Mathematics. 157-176.
[77]
W.D Maurer, State vectors - a preliminary survey, Memorandum M-347, Electronics Research Laboratory, University of California, Berkeley, 1972
[78]
Maurer, W.D., The validity of return address schemes. Information Science. v6 i2. 161-170.
[79]
Mazurkiewicz, A.W., Proving algorithms by tail functions. Information and Control. v18 i3. 220-226.
[80]
McCarthy, J., Recursive functions of symbolic expressions and their computation by machine. Part I. Communications of the ACM. v3 i4. 184-195.
[81]
J. McCarthy, A basis for a mathematical theory of computation, in: Proc. Western Joint Computer Conf., 1961, pp. 225-238
[82]
J. McCarthy, Towards a mathematical science of computation, in: Information Proceedings 1962, Proc. of IFIP Congress 62, Munich, North-Holland, Amsterdam, 1963, pp. 21-28
[83]
J. McCarthy, Problems in the theory of computation, in: Proc. IFIP Congress 65, Washington, Spartan Books, 1965, pp.¿219-222
[84]
McCarthy, J., A formal description of a subset of Algol. In: Steel, T.B. (Ed.), Formal Language Description Languages for Computer Programming, North-Holland, Amsterdam. pp. 1-12.
[85]
McCarthy, J. and Painter, J.A., Correctness of a compiler for arithmetic expressions. In: Proc. Symp. Applied Math., Mathematical Aspects of Computer Science, vol. 19. American Mathematical Society, Providence, RI. pp. 33-41.
[86]
Mealy, G.H., A method for synthesizing sequential circuits. Bell System Technical Journal. v34. 1045-1079.
[87]
Melzak, Z.A., An informal arithmetical approach to computability and computation. Canadian Mathematical Bulletin. v4 i3. 279-293.
[88]
Milner, R., Program schemes and recursive function theory. Machine Intelligence. v5. 39-58.
[89]
Equivalences on program schemes. Journal of Computer and System Sciences. v4 i3. 205-219.
[90]
R. Milner, Implementation and applications of Scott's logic for computable functions, in: Proc. ACM Conf. on Proving Assertions about Programs (SIGPLAN Notices 7(1); SIGACT News 14), January 1972, pp. 1-6
[91]
Milner, R. and Weyhrauch, R.W., Proving compiler correctness in a mechanized logic. Machine Intelligence. v7. 51-70.
[92]
Minsky, M.L., Recursive unsolvability of Post's problem of "Tag" and other topics in the theory of Turing machines. Annals of Mathematics. v74 i3. 437-455.
[93]
Moore, E.F., Gedanken-experiments on sequential machines. In: Annals of Mathematical Studies, vol. 34. Princeton University Press. pp. 129-153.
[94]
Axioms and theorems for a theory of arrays. IBM Journal of Research and Development. v17 i2. 135-175.
[95]
Narasimhan, R., Programming languages and computers: A unified metatheory. Advances in Computers. v8. 189-245.
[96]
Naur, P., Report on the algorithmic language Algol 60. Communications of the ACM. v3 i5. 299-314.
[97]
Proof of algorithms by general snapshots. BIT. v6 i4. 310-316.
[98]
Neuhold, E.J., The formal description of programming languages. IBM Systems Journal. v10 i2. 86-112.
[99]
Orgass, R.J. and Fitch, F.B., A theory of computing machines. Studium Generale. v22. 83-104.
[100]
Orgass, R.J. and Fitch, F.B., A theory of programming languages. Studium Generale. v22. 113-136.
[101]
Some results concerning proofs of statements about programs. Journal of Computer and System Sciences. v4 i1. 74-88.
[102]
J.A. Painter, Semantic correctness of a compiler for an Algol-like language, Ph.D. Thesis, Computer Science Department, Stanford University, 1967
[103]
Park, D., Some semantics for data structures. Machine Intelligence. v3. 351-371.
[104]
Peter, R., Graphschemata und rekursive Funktionen. Dialectica. v12. 373-393.
[105]
Podlovchenko, R.I., On transformations of program schemes and their application to programming. Problems of Cybernetics. v7.
[106]
J.C. Reynolds, Definitional interpreters for higher-order programming languages, in: Proc. ACM National Conference, Boston, 1972, pp. 717-740
[107]
Rutledge, J.D., On Ianov's program schemata. Journal of the ACM. v11 i1. 1-9.
[108]
Scott, D., Some definitional suggestions for automata theory. Journal of Computer and System Sciences. v1 i2. 187-212.
[109]
Scott, D., Outline of a mathematical theory of computation. In: Proc. 4th Annual Conf. on Information Sciences and Systems, Princeton. pp. 169-176.
[110]
Scott, D., The lattice of flow diagrams. In: Lecture Notes in Mathematics 188 (Semantics of Algorithmic Languages), Springer-Verlag, Berlin, Heidelberg, New York. pp. 311-366.
[111]
Shepherdson, J.C. and Sturgis, H.E., Computability of recursive functions. Journal of the ACM. v10 i2. 217-255.
[112]
Skowron, A., Semantic translation of programming languages. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. v17. 39-46.
[113]
Strachey, C., Towards a formal semantics. In: Steel, T.B. (Ed.), Formal Language Description Languages for Computer Programming, North-Holland, Amsterdam. pp. 198-216.
[114]
Suppes, P., Introduction to Logic. 1957. Van Nostrand, Princeton, NJ.
[115]
Turing, A. and Turing, A., On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society (2). v42. 230-265.
[116]
A. Turing, Checking a large routine, in: Report of a Conf. on High Speed Automatic Calculating Machines, University Mathematical Laboratory, Cambridge, 1950, pp. 67-69
[117]
Wagner, E.G., Bounded action machines: Toward an abstract theory of computer structure. Journal of Computer and System Sciences. v2 i1. 13-75.
[118]
Wegner, P., Three computer cultures: computer technology, computer mathematics, and computer science. Advances in Computers. v10. 7-78.
[119]
Wegner, P., The Vienna definition language. Computing Surveys. v4 i1. 5-63.
[120]
R. Weyhrauch, R. Milner, Program semantics and correctness in a mechanized logic, in: Proc. 1st USA-Japan Computer Conference, Tokyo, 1972, pp. 384-390
[121]
Wilkes, M.V., The outer and inner syntax of a programming language. Computer Journal. v11 i3. 260-263.
[122]
W. Wilner, Declarative semantic definition, Ph.D. Thesis, Computer Science Department, Stanford University, 1971
[123]
Wirth, N. and Weber, H., EULER: A generalization of Algol, and its formal definition. Communications of the ACM. v9. 13-25.
[124]
Yanov, Yu.I., On the logical schemes of algorithms. Problems of Cybernetics. v1. 82-140.
[125]
Younger, D.H., Minimum feedback arc sets for a directed graph. IEEE Transactions on Circuit Theory CT-10. v2. 238-245.
Index Terms
- Survey: A survey of state vectors
Recommendations
Survey calculations
One of my passions in life is to try and understand how we have developed the wonderful calculating ability we currently possess. Anyone with this hobby will undoubtedly start by looking back to see how the first PCs were developed, then progress back ...
Research Survey on Support Vector Machine
MOBIMEDIA'17: Proceedings of the 10th EAI International Conference on Mobile Multimedia CommunicationsSupport vector machine (SVM) as a learning machine has shown a good learning ability and generalization ability in classification, regression and forecasting. Because of its excellent learning performance, SVM has always been a hotspot in machine ...
Survey calculations
ITiCSE-WGR '04: Working group reports from ITiCSE on Innovation and technology in computer science educationOne of my passions in life is to try and understand how we have developed the wonderful calculating ability we currently possess. Anyone with this hobby will undoubtedly start by looking back to see how the first PCs were developed, then progress back ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier Ltd © 2008.
Publisher
Elsevier Science Publishers B. V.
Netherlands
Publication History
Published: 01 April 2008
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 24 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in