SECD machine

?

對程序語言理論的理解 程序語言理論主要研究語法、語義及語言的實現。
編程語言有語法，各種數學邏輯、結構化數據都有語法。
喬姆斯基的語言體系及巴科斯范式是語法分析的基礎，語法分析將字符串轉換成有結構的抽象語法數據。對于語法的結構化表示，在命令式語言中使用數據結構，在函數式語言中使用列表或者自定義的數據類型。
函數式語言的抽象性使人常常忘記了語法分析。
歸納和遞歸是集合論、邏輯、計算理論的基礎概念，同樣也是程序語言理論的核心概念。

語言的實現方式包括編譯和解釋，對其理解的關鍵是環境和作用域，函數式語言天生適合這些任務。
解釋型的實現包括高級的(抽象機、求值器)和低級的(編譯器+虛擬機)，它們之間可以相互轉換。對于lambda演算，Bruijn編碼，CPS轉換，閉包轉換是實現的基本工具。虛擬機有CAM,VEC,Zinc等，抽象機有Krivine,CEK,CLS,SECD等。Krivine,CEK是基于所謂的標準語義，分別使用傳名調用和傳值調用。CLS,SECD基于棧語義。
函數式語言的簡單、高階等特點使得函數式編程變化多樣，出現許多不尋常的編程方法和模式，如monad。

類型論的研究包括語言中的應用和數學邏輯中的應用。這兩個方面是相互聯系的，相互借鑒的。語言中的類型系統設計要在靈活和表達性之間權衡，類型在程序優化、安全性、可擴展性、并行化、軟件維護等方面都有應用。對于數學中的應用，類型論主要研究構造邏輯在類型論中的表示和推理，同時通過證明的構造可以獲得滿足特定規格的程序。

?

來源：?<http://www.douban.com/note/267421836/>

?

范疇與程序語言 這里不是討論哲學一般意義上的范疇，而是從數學的角度。

范疇是由一組對象和滿足一定條件的態射組成的。
兩個范疇之間的映射稱為函子，而自然變換則是描述兩個函子之間的關系。
基于以上的幾個概念，范疇論能夠作為數學基礎語言代替集合論。大部分人已經習慣了集合論的直覺方式，所以理解范疇論就顯得抽象多了。

將typed lambda 演算的類型視為對象，函數視為態射，則lambda 演算構成一個范疇。
笛卡爾閉范疇是指笛卡爾積（×），態射（→）封閉，它與含多參數函數、高階函數的lambda演算形成的范疇等價。

monad利用類型系統給類型打上標記，對純空間和非純空間進行隔離，使得使用monad類型的函數永遠返回monad類型，提供do語法模擬命令式風格。純世界可進入非純世界，在非純世界中可以使用純世界的數據，卻最終無法逃脫非純世界。

?

來源：?<http://www.douban.com/note/144607646/>

?

基于棧與基于寄存器的區別

基于寄存器的虛擬機：
1、使用堆棧來分配激活記錄器
2、基于寄存器代碼免去了使用push和pop命令的麻煩，減少了每個函數的指令總數。
3、代碼尺寸和解碼效率不如基于棧虛擬機，因為它包含操作數，所以指令大于基于堆棧的指令。但是基于寄存器產生更少的代碼，所以總的代碼數不會增加。
4、寄存器虛擬機必須從操作指令中解碼操作數，需要額外的解碼操作。

基于棧的虛擬機：
1、代碼必須使用這些指令來移動變量(即push和pop)
2、代碼尺寸小和解碼效率會更高些
3、堆棧虛擬機指令有隱含的操作數。

來源：?<https://blog.csdn.net/strliu/article/details/7906017?>

SECD machine

From Wikipedia, the free encyclopedia

The?SECD machine?is a highly influential?virtual machine?and?abstract machine?intended as a target for?functional programming language?compilers. The letters stand for?Stack,?Environment,Control,?Dump, the internal registers of the machine. These registers point to?linked lists?in memory.

The machine was the first to be specifically designed to evaluate?lambda calculus?expressions. It was originally described by?Peter J. Landin?as part of his?ISWIM programming language?definition in 1963. The description published by Landin was fairly abstract, and left many implementation choices open (like an?operational semantics). Hence the SECD machine is often presented in a more detailed form, such as?Peter Henderson's?Lispkit Lisp?compiler, which has been distributed since 1980. Since then it has been used as the target for several other experimental compilers.

In 1989 researchers at the?University of Calgary?worked on a hardware implementation of the machine.^[1]

?

Contents

??[hide]?

• 1?Informal description
• 2?Registers and memory
• 3?Instructions
• 4?References
• 5?Further reading
• 6?External links

?

Informal description[edit]

When evaluation of an expression begins, the expression is loaded as the only element of?C. The environment?E, stack?S?and dump?D?begin empty.

During evaluation of?C?it is converted to?reverse Polish notation?with?ap?(for?apply) being the only operator. For example, the expression F (G X) (a single list element) is changed to the list X:G:ap:F:ap.

Evaluation of?C?proceeds similarly to other RPN expressions. If the first item in?C?is a value, it is pushed onto the stack?S. More exactly, if the item is an identifier, the value pushed onto the stack will be the binding for that identifier in the current environment?E. If the item is an abstraction, a?closure?is constructed to preserve the bindings of its free variables (which are in?E), and it is this closure which is pushed onto the stack.

If the item is?ap, two values are popped off the stack and the application done (first applied to second). If the result of the application is a value, it is pushed onto the stack.

If the application is of an abstraction to a value, however, it will result in a lambda calculus expression which may itself be an application (rather than a value), and so cannot be pushed onto the stack. In this case, the current contents of?S,?E, and?C?are pushed onto?D?(which is a stack of these triples),?S?is reinitialised to empty, and?C?is reinitialised to the application result with?E?containing the environment for the free variables of this expression, augmented with the binding that resulted from the application. Evaluation then proceeds as above.

Completed evaluation is indicated by?C?being empty, in which case the result will be on the stack?S. The last saved evaluation state on?D?is then popped, and the result of the completed evaluation is pushed onto the stack contents restored from?D. Evaluation of the restored state then continues as above.

If?C?and?D?are both empty, overall evaluation has completed with the result on the stack?S.

Registers and memory[edit]

The SECD machine is?stack-based. Functions take their arguments from the stack. The arguments to built-in instructions are encoded immediately after them in the instruction stream.

Like all internal data-structures, the stack is a list, with the?S?register pointing at the list's?head?or beginning. Due to the list structure, the stack need not be a continuous block of memory, so stack space is available as long as there is a single free memory cell. Even when all cells have been used,?garbage collection?may yield additional free memory. Obviously, specific implementations of the SECD structure can implement the stack as a canonical stack structure, so improving the overall efficiency of the virtual machine, provided that a strict bound be put on the dimension of the stack.

The?C?register points at the head of the code or instruction list that will be evaluated. Once the instruction there has been executed, the?C?is pointed at the next instruction in the list—it is similar to an?instruction pointer?(or?program counter) in conventional machines, except that subsequent instructions are always specified during execution and are not by default contained in subsequent memory locations, as it is the case with the conventional machines.

The current variable environment is managed by the?E?register, which points at a list of lists. Each individual list represents one environment level: the parameters of the current function are in the head of the list, variables that are free in the current function, but bound by a surrounding function, are in other elements of?E.

The dump, at whose head the?D?register points, is used as temporary storage for values of the other registers, for example during function calls. It can be likened to the return stack of other machines.

The memory organization of the SECD machine is similar to the model used by most functional language?interpreters: a number of memory cells, each of which can hold either an?atom?(a simple value, for example?13), or represent an empty or non-empty list. In the latter case, the cell holds two pointers to other cells, one representing the first element, the other representing the list except for the first element. The two pointers are traditionally named?car?and?cdr?respectively—but the more modern terms?head?and?tail?are often used instead. The different types of values that a cell can hold are distinguished by a?tag. Often different types of atoms (integers, strings, etc.) are distinguished as well.

So a list holding the numbers?1,?2, and?3, usually written as "(1 2 3)", could be represented as follows:

Address Tag Content (value for integers, car & cdr for lists)9 [ integer | 2 ]8 [ integer | 3 ]7 [ list | 8 | 0 ]6 [ list | 9 | 7 ]...2 [ list | 1 | 6 ]1 [ integer | 1 ]0 [ nil ]

The memory cells 3 to 5 do not belong to our list, the cells of which can be distributed randomly over the memory. Cell 2 is the head of the list, it points to cell 1 which holds the first element's value, and the list containing only?2?and?3?(beginning at cell 6). Cell 6 points at a cell holding 2 and at cell 7, which represents the list containing only?3. It does so by pointing at cell 8 containing the value?3, and pointing at an empty list (nil) as cdr. In the SECD machine, cell 0 always implicitly represents the empty list, so no special tag value is needed to signal an empty list (everything needing that can simply point to cell 0).

The principle that the cdr in a list cell must point at another list is just a convention. If both car and cdr point at atoms, that will yield a pair, usually written like "(1 . 2)"

Instructions[edit]

• nil?pushes a nil pointer onto the stack
• ldc?pushes a constant argument onto the stack
• ld?pushes the value of a variable onto the stack. The variable is indicated by the argument, a pair. The pair's car specifies the level, the cdr the position. So "(1 . 3)" gives the current function's (level 1) third parameter.
• sel?expects two list arguments, and pops a value from the stack. The first list is executed if the popped value was non-nil, the second list otherwise. Before one of these list pointers is made the new?C, a pointer to the instruction following?sel?is saved on the dump.
• join?pops a list reference from the dump and makes this the new value of?C. This instruction occurs at the end of both alternatives of a?sel.
• ldf?takes one list argument representing a function. It constructs a closure (a pair containing the function and the current environment) and pushes that onto the stack.
• ap?pops a closure and a list of parameter values from the stack. The closure is applied to the parameters by installing its environment as the current one, pushing the parameter list in front of that, clearing the stack, and setting?C?to the closure's function pointer. The previous values of?S,?E, and the next value of?C?are saved on the dump.
• ret?pops one return value from the stack, restores?S,?E, and?C?from the dump, and pushes the return value onto the now-current stack.
• dum?pushes a "dummy", an empty list, in front of the environment list.
• rap?works like?ap, only that it replaces an occurrence of a dummy environment with the current one, thus making recursive functions possible

A number of additional instructions for basic functions like car, cdr, list construction, integer addition, I/O, etc. exist. They all take any necessary parameters from the stack.

References[edit]

Jump up^?A paper on the design,?SECD: DESIGN ISSUES?is available.

Further reading[edit]

• Danvy, Olivier.?A Rational Deconstruction of Landin's SECD Machine. BRICS research report RS-04-30, 2004. ISSN 0909-0878
• Field, Anthony J. Field and Peter G. Harrison. 1988?Functional Programming. Addison-Wesley.?ISBN 0-201-19249-7
• Graham, Brian T. 1992 "The SECD Microprocessor: A Verification Case Study". Springer.?ISBN 0-7923-9245-0
• Henderson, Peter. 1980?Functional Programming: Application and Implementation. Prentice Hall.?ISBN 0-13-331579-7
• Kogge, Peter M.?The Architecture of Symbolic Computers.?ISBN 0-07-035596-7
• Landin, P. J.?(January 1964). "The Mechanical Evaluation of Expressions".?Comput. J.?6?(4): 308–320.?doi:10.1093/comjnl/6.4.308.?edit
• Landin, P. J.?(March 1966).?"The next 700 programming languages"?(PDF).?Comm. ACM?9?(3): 157–166.?doi:10.1145/365230.365257.?edit

External links[edit]

• SECD collection

Categories:?

• 1964 in computer science
• Implementation of functional programming languages
• Models of computation
• Abstract machines

來源：?<https://en.wikipedia.org/wiki/SECD_machine> ?

SECD抽象機[編輯]

SECD 機是非常有影響的意圖作為函數式編程語言編譯器目標的虛擬機。SECD 分別是這個機器的內部寄存器的名字的首字母：Stack,?Environment,?Code,?Dump。這些寄存器指向在內存中鏈表。

這種機器最初明確設計用來計算?lambda 演算表達式。最初?Peter J. Landin?在1963年把它作為他的?ISWIM編程語言定義的一部分描述。Landin 出版的描述非常抽象，（象一種操作語義那樣）留下很多實現選擇開放著。所以 SECD 機經常以更具體的形式出現，比如?Peter Henderson?的?Lispkit Lisp?編譯器，它自1980年開始發行。此后它已經被用做多個其他實驗編譯器的目標。

在1989年在卡爾加里大學的研究者制作了這種機器的一個硬件實現。

?

目錄

??[隱藏]?

• 1?寄存器和內存
• 2?指令
• 3?進一步閱讀
• 4?外部鏈接

?

寄存器和內存[編輯]

SECD 機是基于棧的，函數從棧中取得它們的形式參數（parameter）。與之相對，指令的實際參數（argument）跟在指令之后。

棧同所有內部數據結構一樣是個列表，S?寄存器指向這個列表的頭部或開始端。由于列表結構，棧不需要連續成塊的內存，所以只要有一個單一空閑內存單元棧空間就是可獲得的。即使在所有單元都已經使用了時候，垃圾收集仍可以產生額外的空閑內存。

C?寄存器指向要計算的代碼或指令列表的頭部。一旦指令已經被執行，C?就指向在列表中的下一個指令—它類似于常規機器中的“指令指針”（或程序計數器），除了后續指令不需要在后續內存位置上之外。

E?寄存器管理當前變量環境，它指向一個列表的列表。每個單獨列表都代表一個環境級別：當前函數的形式參數位于列表的頭部，在當前函數中自由但受外圍函數約束（bound）的變量在?E?的其他元素中。

D?寄存器指向轉儲（dump）的頭部，它被用做其他寄存器的值的臨時存儲，例如在函數調用期間。它聯系于其他機器的返回棧。

SECD 機的內存組織類似于大多數函數式編程語言解釋器所用的模型：一些內存單元，每個都持有要么一個“原子”（一個簡單值例如“13”），或表示一個空或非空列表。在后者情況，單元持有到其他單元的兩個指針，一個表示第一個元素，另一個表示除去第一個元素之外的列表。這兩個指針傳統上分別叫做?car?和?cdr?— 現在更常使用現代術語“頭”和“尾”。單元持有值的不同類型由一個“標志”來區分。原子的不同類型（整數、字符串等等）經常是同樣可區分的。

所以持有數“1”，“2”和“3”的一個列表，經常寫為“（1 2 3）”，可以表示為如下：

地址 標志 內容(對整數是值，對列表是 car 與 cdr)9 [ integer | 2 ]8 [ integer | 3 ]7 [ list | 8 | 0 ]6 [ list | 9 | 7 ]...2 [ list | 1 | 6 ]1 [ integer | 1 ]0 [ nil ]

內存單元 3 到 5 不屬于這個列表，它的單元可以在內存中隨機分布。單元 2 是這個列表的頭部，它指向持有第一個元素的值的單元 1，和只包含“2”和“3”的（開始于單元 6）列表。單元 6 指向持有“2”的單元，和表示只包含“3”的列表的單元 7。它接著指向持有值“3”的單元 8，和指向空列表（nil）作為 cdr。在 SECD 機中，單元 0 總是暗含表示空列表，所以不需要特殊的標志值來指示空列表（只需要簡單的指向單元 0）。

在列表的單元中 cdr 必須指向另一個列表的原則只是個約定。如果 car 和 cdr 二者都指向原子，則生成一個點對，通常寫為如“（1 . 2）”這樣。

指令[編輯]

• nil?把一個 nil（空）指針壓入棧頂
• ldc?把一個常量實際參數壓入棧頂
• ld?把一個變量的值壓入棧頂。這個變量是由實際參數指示的一個點對。這個點對的 car 指定級別，cdr 指定位置。所以“（1 . 3）”給出當前函數（級別 1）的第三個形式參數。
• sel?期望兩個列表實際參數，并從棧頂彈出一個值。如果彈出的值非 nil 在執行第一個列表，否則執行第二個列表。在這些列表指針之一被作為新的?C?寄存器之前，保存到隨后?sel?的指令的指針到轉儲上。
• join?從轉儲中彈出一個列表引用并把它作為?C?寄存器的新值。這個指令出現在?sel?的兩個選擇二者的結束處。
• ldf?接受表示函數的一個列表實際參數。它構造一個閉包（包含函數和當前環境的一個點對）并把它壓入棧頂。
• ap?從棧頂彈出一個閉包和形式參數值的一個列表。通過安裝這個閉包的環境為當前環境，把形式參數列表壓在它的上面，清空棧，并設置?C?寄存器為這個閉包的函數指針，這樣就把閉包應用于形式參數之上。S,?E寄存器以前的值和?C?寄存器的下一個值被保存到轉儲上。
• ret?從棧頂彈出返回一個值，從轉儲中恢復?S,?E?和?C?寄存器，并把這個返回值壓入現在當前的棧頂。
• dum?把一個“啞元”也就是空列表壓入環境列表的頂部。
• rap?如?ap?那樣工作，唯一不同的是它把啞環境的出現替代為當前環境，因此使遞歸成為可能。

存在一些基本函數的補充指令如 car, cdr，列表構造，整數加法，I/O，等等。它們都必須從棧上取得形式參數。

進一步閱讀[編輯]

• Peter M. Kogge:?The Architecture of Symbolic Computers.?ISBN 0-07-035596-7
• Peter Henderson,?Functional Programming: Application and Implementation. Prentice Hall, 1980.?ISBN 0-13-331579-7
• Anthony J. Field and Peter G. Harrison:?Functional Programming. Addison-Wesley, 1988.?ISBN 0-201-19249-7
• Olivier Danvy：A Rational Deconstruction of Landin's SECD Machine. BRICS research report RS-04-30, 2004. ISSN 0909-0878

外部鏈接[編輯]

• SECD collection
• Original SECD paper，"The Mechanical evaluation of Expressions" P.J. Landin The Computer Journal Vol. 6 pp308-320 1964

分類：

• 計算模型

來源：?<https://zh.wikipedia.org/wiki/SECD%E6%8A%BD%E8%B1%A1%E6%9C%BA> ?

===================?End

?

總結

以上是生活随笔為你收集整理的SECD machine的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。