More Web Proxy on the site http://driver.im/

article

Free access

Linear logic and permutation stacks—the Forth shall be first

Author:

Henry G. BakerAuthors Info & Claims

ACM SIGARCH Computer Architecture News, Volume 22, Issue 1

Pages 34 - 43

https://doi.org/10.1145/181993.181999

Published: 01 March 1994 Publication History

Abstract

Girard's linear logic can be used to model programming languages in which each bound variable name has exactly one "occurrence"---i.e., no variable can have implicit "fan-out"; multiple uses require explicit duplication. Among other nice properties, "linear" languages need no garbage collector, yet have no dangling reference problems. We show a natural equivalence between a "linear" programming language and a stack machine in which the top items can undergo arbitrary permutations. Such permutation stack machines can be considered combinator abstractions of Moore's Forth programming language.

References

[1]

AdaLRM: Reference Manual for the Ada® Programming Language. ANSI/MIL-STD-1815A-1983, U.S. Gov't Print Off., Wash., DC, 1983.

Digital Library

[2]

Aho, A.V., and Johnson, S.C. "Optimal Code Generation for Expression Trees". JACM 23, 3 (July 1976), 488-501.

Digital Library

[3]

Aho, A.V., et al. "Code Generation for Expressions with Common Subexpressions". JACM 24, 1 (Jan. 1977), 146-160.

Digital Library

[4]

Aho, A.V., et al. Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading, MA, 1986.

Digital Library

[5]

Allmark, R.H., & Lucking, J.R. "Design of an Arithmetic Unit Incorporating a Nesting Store". Proc. IFIP 1962, 694-698.

[6]

Backus, J. "Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs". CACM 21, 8 (1978), 613-641.

Digital Library

[7]

Baer, J.-L. Computer Systems Architecture. Computer Science Press, Potomac, MD, 1980.

[8]

Baker, H.G. "Structured Programming with Limited Private Types in Ada: Nesting is for the Soaring Eagles". Ada Letters XI, 5 (1991), 79-90.

Digital Library

[9]

Baker, H.G. "Lively Linear Lisp -- 'Look Ma, No Garbage!'". ACM Sigplan Notices 27,8 (Aug. 1992), 89-98.

Digital Library

[10]

Baker, H.G. "NREVERSAL of Fortune--The Thermodynamics of Garbage Collection". Int'l WIS Mem. Mgmt, St Malo 1992, Springer LNCS 637.

Digital Library

[11]

Baker, H.G. "Metacircular Semantics for Common Lisp Special Forms". ACM Lisp Pointers V,4 (Oct-Dec 1992), 11-20.

Digital Library

[12]

Baker, H.G. "How to Steal from a Limited Private Account". ACM Ada Letters XIII,3 (May/June 1993), 91-95.

Digital Library

[13]

Baker, H.G. "Equal Rights for Functional Objects or, The More Things Change, The More They Are the Same". ACM OOPS Messenger 4,4 (Oct. 1993), 2-27.

Digital Library

[14]

Baker, H.G. "A 'Linear Logic' Quicksort" Subm. to ACM Sigplan Notices, 1993.

[15]

Banker, H.G. "Sparse Polynomials and Linear Logic". Subm. to ACM Sigsam Bulletin, 1993.

Digital Library

[16]

Barton, R.S. "A New Approach to the Functional Desing of a Digital Computer". AFIPS West. Jt. Computer Conf. 19 (1961), 393-396.

[17]

Barton, R.S. "Ideas for Computer Systems Organization: A Personal Survey". In Tou, J.T. Software Engineering, Vol. 1. Acad. Press, 1970.

[18]

Bell, C.G., et al. Computer Engineering: A DEC View of Hardware Systems Design. Digital Press, Bedford, MA, 1978.

Digital Library

[19]

Blake, R.P. "Exploring a Stack Architecture". IEEE Comp. 10,5 (1977), 30-39.

Digital Library

[20]

Brooks, F.P. "Recent Developments in Computer Organization". In Advances in Electronics and Electronic Devices, Acad. Press, NY, 1963.

[21]

Bruno, J., and Sethi, R. "Code Generation for a One-Generation Machine". JACM 23,3 (July 1976), 502-510.

Digital Library

[22]

Bullman, D.M., ed. "Stack Computer". IEEE Comp. 10,5 (May 1977), 14-52.

[23]

Carriero N., & Gelernter, D. "Linda in Context". CACM 32, 4 (1989), 444-458.

Digital Library

[24]

Case, R.P. & Padegs, A. "Architecture of the IBM System/370". CACM 21, 1 (Jan. 1978), 73-96.

Digital Library

[25]

Castan, M., et al. "MaRS: A parallel graph reduction multiprocessor". Comput. Arch. News 16,3 (June 1988), 17-24.

Digital Library

[26]

Cheese, A. "Combinatory Code and a Parallel Packet Based Computational Model". Sigplan Not. 22,4 (April 1987), 49-58.

Digital Library

[27]

Chirimar, J., et al. "Proving Memory Management Invariants for a Language Based on Linear Logic". Proc. ACM Conf. Lisp & Funct. Prog., San Fran., CA, June, 1992, ACM Lisp Pointers V, 1 (Jan.-Mar. 1992), 139.

Digital Library

[28]

Church, A. The Calculi of Lambda-Conversion. Princeton U. Press, 1941.

Digital Library

[29]

Coffman, E.G., Jr., & Sethi, R. "Instruction Sets for Evaluating Arithmetic Expressions". JACM 30,3 (July 1983), 457-478.

Digital Library

[30]

Collins, G.E. "A method for overlapping and erasure of lists". CACM 3, 12 (Dec. 1960), 655-657.

Digital Library

[31]

Cragon, H.G. "An Evaluation of Code Space Requirements and Performance of Various Architectures". Comput. Arch. News 7,5 (Feb. 1979), 5-21.

Digital Library

[32]

Curry, H., and Feys, R. Combinatory Logic. North-Holland, 1958.

[33]

Dahl, O.-J., Nygaard. "Simula-an Algol-Based Simulation Language". CACM 9,9 (1966), 671-678.

Digital Library

[34]

Darlington, J., & Reeve, M. "ALICE--A Multiprocessor Reduction Machine for the Evaluation od Applicative Languages". Proc. FPCA, 1981.

Digital Library

[35]

Denning, P.J. "A Question of Semantics". Comput. Arch. News 6,8 (April 1978), 16-18. Discusses stack architectures.

Digital Library

[36]

Deutsch, L.P. "A Lisp Machine with Very Compact Programs". Proc. IJCAI 3, Stanford, CA, 1973.

[37]

Doran, R.W. "Architecture of Stack Machines". In Chu, Y., ed. High-Level Language Computer Architecture. Acad. Press, NY, 1975, pp. 63-108.

[38]

Fasel, J.H., et al, eds. "Sigplan Notices Special Issue on the Functional Programming Language Haskell". Sigplan Not. 27,5 (May 1992).

[39]

Francis, R.S. "Containment Defines a Class of Recursive Data Structures". Sigplan Not. 18,4 (Apr. 1983), 58-64.

Digital Library

[40]

Friedman, D.P., & Wise, D.S. "Aspects of applicative programming for parallel processing". IEEE Trans. Comput. C-27, 4 (Apr. 1978), 289-296.

Digital Library

[41]

Gabriel R.P. "The Why of Y". Lisp Pointer 2,2 (Oct.-Dec. 1988), 15-25.

[42]

Girard, J.-Y. "Linear Logic". Theoretical Computer Sci. 50 (1987), 1-102.

Digital Library

[43]

Glass, H. "Threaded Interpretive Systems and Functional Programming Environments". Sigplan Not. 20,4 (Apr. 1985), 24-32.

Digital Library

[44]

Goldberg, A., and Robson, D. Smalltalk-80: The Language and Its Implementatoin. Addison-Wesley, Readig, MA 1983.

Digital Library

[45]

Grabienski, P. "FLIP-FLOP: A Stack-Oriented Multiprocessing System". Proc. 2nd Symp. on Parallel Algs. and Archs., Crete, July, 1990, 161-168.

Digital Library

[46]

Halstead, R.H. "Overview of Concert Multilisp: A Multiprocessor Symbolic Computing System". Comput. Arch. News 15,1 (Mar. 1987), 5-14.

Digital Library

[47]

Hanson, C. "Efficient Stack Allocation for Tail-Recursive Languages". ACM Conf. Lisp & Funct. Progr., 1990, Nice France, 106-118.

Digital Library

[48]

Harms, D.E., & Weide, B.W. "Copying and Swapping: Influences on the Design of Reusable Software Components". IEEE Tr. SE 17,5 (1991), 424-435.

Digital Library

[49]

Harrison, P.G., & Khoshnevisan, H. "Efficient Compilation of Linear Recursive Functions into Object Level Loops". Symp. on Compiler Constr. '86, Sigplan Not. 21, 7 (July 1986), 207-218.

Digital Library

[50]

Hauck, E.A., and Dent, B.A. "Burroughs B6500/B7500 Stack Mechanism". AFIPS Spring Jt. Computer Conf. 32 (1968), 245-251.

Digital Library

[51]

Hayes, J.R., et al. "An Architecture for the Direct Execution of the Forth Programming Language". ASPLOS II, Sigplan Not. 22,10 (1987), 42-49.

[52]

Herlihy, M. "Wait-Free Synchronization". TOPLAS 11, 1 (1991), 124-149.

Digital Library

[53]

Hesselink, W.H. "Axioms and Models of Linear Logic". Formal Aspects of Comput. 2,2 (Apr-June 1990). 139-166.

[54]

Hewitt, C., & Baker, H. "Laws for Communicating Parallel Processes". IFIP 77 Proceedings, North-Holland.

[55]

Hill, D.D. "An Analysis of C Machine Support for Other Block-Structured Languages", Comput. Arch. News 11,4 (Sept. 1983), 6-16.

Digital Library

[56]

Hudak, P. "Conception, evolution and application of functional programming languages". ACM Comput. Surv. 21,3 (Sept. 1989). 359-411.

Digital Library

[57]

Hughes, J. "Why functional programming matters". The Computer J. 32,2 (April 1989), 98-107.

Digital Library

[58]

Ito, T., and Halstead, Jr., R.H., Eds. Parallel Lisp: Language and Systems. Springer LNCS 441, 1990.

[59]

James, J.S. "FORTH for Microcomputers". Sigplan Not. 13,10 (1978), 33-39.

Digital Library

[60]

Keedy, J.L. "On the Use of Stacks in the Evaluation of Expressions". Comput. Arch. News 6,6 (Feb. 1978), 22-28.

Digital Library

[61]

Keedy, J.L. "On the Evaluation of Expressions using Accumulators, Stacks and Store-to-Store Instructions". Comput. Arch. News 7,4 (1978), 24-27.

Digital Library

[62]

Keedy, J.L. "More on the Use of Stacks in the Evaluations of Expressions". Comput. Arch. News 7,8 (June 1979), 18-21.

Digital Library

[63]

Keller, R.M., and Lin, F.C. "Simulated Performance of a Reduction-Based Multiprocessor. IEEE Computer (July 1984), 70-82.

[64]

Keown, W.F., Jr., et al. "Performance of the Harris RTX 2000 Stack Architecture versus the Sun4 SPARC and the Sun3 M68020 Architecture". Comput. Arch. News 20,3 (June 1992).

Digital Library

[65]

Kieburtz, R.B. "Programming without pointer variables". Proc. Conf. on Data: Abstr., Defn. and Struct., Sigplan Not. 11 (Spec. iss. 1976), 95-107.

[66]

Kieburtz, R.B. "The G-machine: a fast, graph-reduction evaluator". Proc. IFIP FPCA, Nancy, France, 1985.

Digital Library

[67]

Kingdon, H, et al. "The HDG-machine: a highly distributed graph-reducer for a transputer network". The Computer J. 34,4 (1991), 290-301.

Digital Library

[68]

Koopman, P. Stack Computers, The New Wave. Ellis Horwood, Chichester, W. Sussex, England, 1989.

Digital Library

[69]

Koopman, P., & Lee, P. "A Fresh Look at Combinator Graph Reduction". ACM PLDI'89, Sigplan Not. 24,7 (1989), 110-119.

Digital Library

[70]

Koopman, P.J., Jr., et al. "Cache Behavior of Combinator Graph Reduction". ACM TOPLAS 14,2 (April 1992), 265-297.

Digital Library

[71]

Lafont, Y. "The Linear Abstract Machine". Th. Comp. Sci. 59 (1988), 157-180.

Digital Library

[72]

Lawson, H.W., Jr. "Programming-Language-Oriented Instruction Streams". IEEE Trans. Comput. C-17,5 (1968), 476-485. Discusses stacks.

Digital Library

[73]

Lieu, C.T., & Sarni, D. "O. Lisp Theoretical Basis and Description". Sigplan Not. 25,12 (Dec. 1990), 37-44.

Digital Library

[74]

Lipovski, G.J. "Just a Few More Words on Microprocessors of the Future". Comput. Arch. News 6,6 (Feb. 1978), 18-21.

Digital Library

[75]

Lonergan, W., & King, P. "Design of the B5000 System". Datamation 7,5 (1961), 28-32.

[76]

Lunde, Å. "Empirical Evaluation of Some Features of Instruction Set Processor Architectures". CACM 20,3 (Mar. 1977), 143-153.

Digital Library

[77]

Martí-Oliet, N., & Meseguer, J. "From Petri nets to linear logic". Math. Struct. in Comp. Sci. 1,1 (Mar. 1991). 69-101.

[78]

Mason, I.A. The Semantics of Destructive Lisp. CSLI LN 5, Stanford, CA, 1986.

Digital Library

[79]

Mattson, R.L., et al. "Evaluation Techniques for Storage Hierarchies". IBM Sys. J. 9,2 (1970), 78-117.

Digital Library

[80]

Maurer, W.D. "A Theory of Computer Instructions". JACM 13,2 (1966), 226-235.

Digital Library

[81]

McKeeman, W.M. "Stack Processors". In Stone, H., ed. Introduction to Computer Architecture. SRA, Chicago, 1975, pp. 281-317.

[82]

Moore, C.H. "The Evolution of Forth, An Unusual Language". Byte 5,8 (Aug. 1980), 76-92.

[83]

Moore, C.H. Personal communication, Aug. 18, 1993.

[84]

Myers, G.J. "The Case Against Stack-Oriented Instruction Sets". ACM Sigarch News 6,3 (Aug. 1977), 7-10.

Digital Library

[85]

Myers, G.J. "The Evalution of Expressions in a Storage-to-Storage Architecture". Comput. Arch. News 6,9 (June 1978), 20-23.

[86]

Nordstrom, D.J. "Threading Lisp". Sigplan Not. 25, 2 (Feb. 1990), 17-24.

Digital Library

[87]

Omondi, A.R. "On function languages and parallel computers". Fut. Gen. Comput. Sys. 6,4 (Sept. 1991), 355-372.

[88]

Osborne, Tom. Personal communication, Aug. 27, 1993.

[89]

Passia, J., and Löhr, K.-P. "Fips: A Functional-Imperative Language for Exploratory Programming". Sigplan Not. 28,5 (May 1993), 39-48.

Digital Library

[90]

Patterson, D.A., and Ditzel, D.R. "The Case for the Reduced Instruction Set Computer". Comput. Arch. News 8,6 (Oct. 1980), 25-32.

Digital Library

[91]

Peyton-Jones, S.L., & Salkild, J. "The Spineless Tagless G-machine". ACM FPCA 4, (1989), 184-201.

Digital Library

[92]

Ponder, C.G., et al. "Are Applicative Languages Inefficient?" Sigplan Not. 23,6 (June 1988), 135-139.

Digital Library

[93]

Prabhala, B., & Sethi, R. "Efficient Computation of Expressions with Common Subexpressions". JACM 27,1 (Jan. 1980), 146-163.

Digital Library

[94]

Randell, B., & Russell, L. Algol 60 Implementation. Acad. Press., 1964.

Digital Library

[95]

Rather, E.D., et al. "The Evolution of Forth". HOPL-II, Sigplan Not. 28,3 (Mar. 1993), 177-199.

Digital Library

[96]

Robison, A.D. "The Illinois Functional Programming Interpreter". Symp. on Interp. and Interpretive Techs., Sigplan Not. 22,7 (July 1987), 64-73.

Digital Library

[97]

Ryer, M.J. Programming in HALIS. Intermetrics, Inc., Camb., MA, 1978.

[98]

Sarwar, S.M. et al. "Implementing Functional Languages on a Combinator-Based Reduction Machine". Sigplan Not. 23,4 (Apr. 1988), 65-70.

Digital Library

[99]

Shalit, A. Dylan^TM: An object-oriented dynamic language. Apple Computer, Camb., MA, 1992.

[100]

Sites, R.L. "A Combined Register-Stack Architecture", Comput. Arch. News 6,8 (April 1978), 19.

Digital Library

[101]

Smith. A.J. "Cache Memories". Comput. Surv. (Sept. 1982), 473-530.

Digital Library

[102]

Steele, G.L. Rabbit: A Compiler for SCHEME (A Study in Compiler Optimization). AI-TR-474, MIT AI Lab., May 1978.

Digital Library

[103]

Steele, G.L. Common Lisp, The Language; 2nd Ed. Digital Press, 1990.

Digital Library

[104]

Stevenson, J.W. "Efficient Encoding of Machine Instructions". Comput. Arch. News 7,8 (June 1979), 10-17.

Digital Library

[105]

Strom, R.E. "Mechanisms for Compile-Time Enforcement of Security". Proc. POPL 10, Jan. 1983.

Digital Library

[106]

Stroustrup, B. The C++ Programming Language. Addison-Wesley, 1986.

Digital Library

[107]

Suzuki, N. "Analysis of Pointer 'Rotation'". CACM 25, 5 (1982), 330-335.

Digital Library

[108]

Tanenbaum, A.S. "Implications of Structured Programming for Machine Architecture". CACM 21,3 (Mar, 1978), 237-246.

Digital Library

[109]

Vegdahl, S.R. "A Survey of Proposed Architectures for the Execution of Functional Languages". IEEE Trans. Comput. C-33,12 (1984), 1050-1071.

Digital Library

[110]

Wadler, P. "Linear types can change the world!". IFIP TC2 Conf. on Progr. Concepts & Meths., April 1990.

[111]

Wadler, P. "Is there a use for linear logic?". Proc. ACM PEPM'91, New Haven, June 1991, 255-273.

Digital Library

[112]

Wakeling. D., & Runciman, C. "Linearity and Laziness". Proc. Funct. Progr. & Comp. Arch., LNCS 523, Springer-Verlag, Aug. 1991, 215-240.

Digital Library

[113]

Wirth, N. "Stack vs. Multiregister Computers". Sigplan Not. (Mar. 1968), 13-19.

Cited By

Stoddart BLynas RZeyda F(2010)A Virtual Machine for Supporting Reversible Probabilistic Guarded Command LanguagesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2010.02.005253:6(33-56)Online publication date: 1-Mar-2010
https://dl.acm.org/doi/10.1016/j.entcs.2010.02.005
Toffoli TCapobianco SMentrasti P(2008)When–and how–can a cellular automaton be rewritten as a lattice gas?Theoretical Computer Science10.1016/j.tcs.2008.04.047403:1(71-88)Online publication date: 1-Aug-2008
https://dl.acm.org/doi/10.1016/j.tcs.2008.04.047
Okasaki CChakravarty M(2002)Techniques for embedding postfix languages in HaskellProceedings of the 2002 ACM SIGPLAN workshop on Haskell10.1145/581690.581699(105-113)Online publication date: 3-Oct-2002
https://dl.acm.org/doi/10.1145/581690.581699
Show More Cited By

Index Terms

Linear logic and permutation stacks—the Forth shall be first

Recommendations

Permutation tableaux and permutation patterns

In this paper we introduce and study a class of tableaux which we call permutation tableaux; these tableaux are naturally in bijection with permutations, and they are a distinguished subset of the -diagrams of Alex Postnikov [A. Postnikov, Webs in ...
On the sign-imbalance of permutation tableaux

Permutation tableaux were introduced by Steingrmsson and Williams. Corteel and Kim defined the sign of a permutation tableau in terms of the number of unrestricted columns. The sign-imbalance of permutation tableaux of length n is the sum of signs over ...
The sorting index and permutation codes

In the combinatorial study of the coefficients of a bivariate polynomial that generalizes both the length and the reflection length generating functions for finite Coxeter groups, Petersen introduced a new Mahonian statistic sor, called the sorting ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGARCH Computer Architecture News

ACM SIGARCH Computer Architecture News Volume 22, Issue 1

Special issue: panel sessions of the 1991 workshop on multithreaded computers

March 1994

61 pages

ISSN:0163-5964

DOI:10.1145/181993

Editor:
Doug DeGroot
Texas Instruments, Inc., Dallas, TX

Issue’s Table of Contents

Copyright © 1994 Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 1994

Published in SIGARCH Volume 22, Issue 1

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
1,251
Total Downloads

Downloads (Last 12 months)932
Downloads (Last 6 weeks)23

Reflects downloads up to 27 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Stoddart BLynas RZeyda F(2010)A Virtual Machine for Supporting Reversible Probabilistic Guarded Command LanguagesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2010.02.005253:6(33-56)Online publication date: 1-Mar-2010
https://dl.acm.org/doi/10.1016/j.entcs.2010.02.005
Toffoli TCapobianco SMentrasti P(2008)When–and how–can a cellular automaton be rewritten as a lattice gas?Theoretical Computer Science10.1016/j.tcs.2008.04.047403:1(71-88)Online publication date: 1-Aug-2008
https://dl.acm.org/doi/10.1016/j.tcs.2008.04.047
Okasaki CChakravarty M(2002)Techniques for embedding postfix languages in HaskellProceedings of the 2002 ACM SIGPLAN workshop on Haskell10.1145/581690.581699(105-113)Online publication date: 3-Oct-2002
https://dl.acm.org/doi/10.1145/581690.581699
Baker H(1995)“Use-once” variables and linear objectsACM SIGPLAN Notices10.1145/199818.19986030:1(45-52)Online publication date: 3-Jan-1995
https://dl.acm.org/doi/10.1145/199818.199860
Baker H(1993)The Boyer benchmark meets linear logicACM SIGPLAN Lisp Pointers10.1145/181889.181890VI:4(3-10)Online publication date: 1-Oct-1993
https://dl.acm.org/doi/10.1145/181889.181890

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents