每日彙整: 2019-03-31

樹莓派、樹莓派之學習、樹莓派之教育

Rock It 《ML》JupyterLab 【丁】Code《七》語義【六】解讀‧四‧Redex 二

假使說給定了一個『 λ表達式』 (\lambda x. ((\lambda y. (x \ y)) \ \Box) \ \bigcirc)，有人『第一步』這樣作『 \beta 化約』︰

((\lambda y. ( \bigcirc \ y)) \ \Box )

，也有人『第一步』這樣作『 \beta 化約』︰

(\lambda x. ( (x \ \Box ) \ \bigcirc)

，這樣不同的『步驟選擇』是否會產生『不同結果』的呢？如果說再次繼續進行『 \beta 化約』，兩者都會得到︰

(\bigcirc \ \Box )

，於是我們就可以歸結的說『 \beta 化約』不管是用著怎麽樣的『步驟次序』，都一定能夠得到『相同結果』的嗎？？

為了考察不同次序步驟的『化約策略』，首先讓我們定義『單步 \beta 化約』︰

A \equiv_{\beta^1} B

是指表達式 B 是經由表達式 A 中的某一函式應用子表達式 C =_{df} ((\lambda x. M) N) 『 \beta 化約』而得來。假使『約定』零步 \beta 化約是說 『A \equiv_{\beta^0} A』，這樣我們就可以說『單步』或『多次單步』之『單步 \beta 化約』的『化約封閉性』︰

U \equiv_{\beta^*} V

，是講存在一個『單步 \beta 化約』的『序列』

U =_{df} S_1, S_2, S_3, \cdots, S_k, S_{k+1}, \cdots, S_n =_{df} V, \ S_k \equiv_{\beta^1} S_{k+1}, k=1\cdots n

。某一表達式 U 我們稱它是『 \beta 可化約』\beta-redex 是指這個表達式還有『未化約』的子應用表達式 ((\lambda x. M) N) 。如果經過『有限的』化約序列，最終抵達一個『沒有未化約』的表達式 V，也就是說 V 中沒有 \beta-redex，這時我們將 V 稱之為『 \beta 正規元型』normal form。於是我們就可以問︰

各種不同的『化約序列』如果存在『 \beta 正規元型』，那它們是相同的嗎？

【Church-Rosser 定理】說

如果 P \equiv_{\beta^*} Q 而且 P \equiv_{\beta^*} R；那麼就會存在一個 S， 使得 Q \equiv_{\beta^*} S 以及 R \equiv_{\beta^*} S。

所以可以講不同的『化約序列』之『 \beta 正規元型』，除了其內函式中的『受約束變元』之『虛名』不同外 ── 可以作『 \alpha 變換』使之一樣 ──，都是『相同的』。這是一個非常重要的歸結，設想萬一它不是這樣，那所謂的『計算』不就成『笑話』了嗎！然而需要小心的是『 \beta 化約』是『單行道』，也就是說 A \equiv_{\beta} B 成立，並不代表 B \equiv_{\beta} A 正確。比方講 ((\lambda x. x) a) \equiv_{\beta} a，從結果變元 a 又要怎麼得回原來函式應用的呢？

那麼『 \beta 化約策略』Reduction Strategy 又是什麼呢？它是一個『函式』RS，可以定義如下︰

一、『定義域』與『對應域』是『所有的 λ 表達式』構成的集合

二、如果 e 是一個『 \beta 正規元型』，RS(e) = e

三、假使 m 不是『 \beta 正規元型』，化約策略會依據特定方式選擇 m 中的某一『優先』 \beta-redex 子表達項 t，RS(m) = t

這樣看來 RS 函式選擇了特定的『步驟次序』── 策略 ── 來作『單步 \beta 化約』，這也是『程式』之『最佳化』optimize 的源起。然而不是每種『化約策略』都能夠抵達存在的『 \beta 正規元型』。舉例說兩種簡單的『左』和『右』化約策略，它總是優先選擇表達式中的『最左』與『最右』 \beta-redex 子表達項 。

TIW

考慮用『左右』策略化約下面的表達式

(((\lambda x. (\lambda y. x)) (\lambda z. z)) (\lambda w. (w w)))

。

用『左』策略會得到『上圖』，用『右』策略會卡在 (\lambda w. (w w))。

所謂的『正規策略』是說用這個策略能夠得到『所有可能存在的』 \beta 正規元型。事實上從邏輯推理可以證明『最左優先』策略是一種『正則策略』，果真是『天左旋』的乎！！

最後讓我們談談『相等』的概念以及『等號 =』的使用，相等和『邏輯推導規則』有關︰

一、 \frac{}{X = X}，無條件自反律

二、 \frac{X = Y}{Y = X}，對稱律

三、 \frac{X = Y \wedge Y = Z}{X = Z}，遷移律

此處的 \frac{Premises}{Conclusion} 是講，如果由『前提』Premises，我們可以邏輯上推導出『結論』Conclusion。也就是說這是廣義的『相等』關係的『內涵』。

此處雖然並不定義『 λ 運算』中所謂的『等式』到底是指什麼？只是從『基元』觀點下，就是說假設我們基本『知道』或者『同意』兩個表達式『A = B』所指的意義── 比方說指相同的計算結果 ──，於是我們可以提出下面的『 λ 理論』︰

一、 \frac{M = N}{(A M) = (A N)}，『應用』於『等式』之『結果』相等

二、 \frac{M = N}{(M A) = (N A)}，『等式』之『函式』的『應用』相等

三、 \frac{M = N}{(\lambda x. M) = (\lambda x.N)}，『等式』之『函式抽象』相等

四、 \frac{}{((\lambda x. M) A) = M[x := A]}，『應用』是無條件的『化約相等』

五、 \eta 擴張， \frac{}{(\lambda x. (M x)) = M}，『外延』相同的『函式』相等

漣漪

干涉

 

簡單的將『變元』、『函式』和『應用』結構起來形成的『 λ 運算』，彷彿是『概念』的『水滴』墜落『心湖』，激起『思想』的『浪花』。這些『浪花』彼此『碰撞』，掀起陣陣『漣漪』，最後『波光』點點，早就分不清哪兒是『始點』，哪兒又是『終點』！！

─── 《Λ 運算︰概念導引《四》》

 

知道 \lambda - redex 是什麼。且能將之聯繫上 PLT

Programming language theory

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features. It falls within the discipline of computer science, both depending on and affecting mathematics, software engineering, linguistics and even cognitive science. It is a well-recognized branch of computer science, and an active research area, with results published in numerous journals dedicated to PLT, as well as in general computer science and engineering publications.

History

In some ways, the history of programming language theory predates even the development of programming languages themselves. The lambda calculus, developed by Alonzo Church and Stephen Cole Kleene in the 1930s, is considered by some to be the world’s first programming language, even though it was intended to model computation rather than being a means for programmers to describe algorithms to a computer system. Many modern functional programming languages have been described as providing a “thin veneer” over the lambda calculus,[1] and many are easily described in terms of it.

The first programming language to be invented was Plankalkül, which was designed by Konrad Zuse in the 1940s, but not publicly known until 1972 (and not implemented until 1998). The first widely known and successful high-level programming language was Fortran, developed from 1954 to 1957 by a team of IBM researchers led by John Backus. The success of FORTRAN led to the formation of a committee of scientists to develop a “universal” computer language; the result of their effort was ALGOL 58. Separately, John McCarthy of MIT developed the Lisp programming language (based on the lambda calculus), the first language with origins in academia to be successful. With the success of these initial efforts, programming languages became an active topic of research in the 1960s and beyond.

 

大體明白 PLT Redex 名目也︰

Welcome

PLT Redex is a domain-specific language designed for specifying and debugging operational semantics. Write down a grammar and the reduction rules, and PLT Redex allows you to interactively explore terms and to use randomized test generation to attempt to falsify properties of your semantics.

PLT Redex is embedded in Racket, meaning all of the convenience of a modern programming language is available, including standard libraries (and non-standard ones) and a program-development environment.

Getting started: Install Racket, and try the tutorial.

Book: Semantics Engineering with PLT Redex (SEwPR) by Matthias Felleisen,Robert Bruce Findler, and Matthew Flatt gives the mathematical background for operational semantics, as well as a tutorial introduction to Redex. The preface, table of contents, and an example syllabus are available online. The book is available fromMIT Press.

Documentation: The reference manual contains all of the gory details of all of Redex’s operators.

Citation: If you use a reduction semantics and/or you modeled a reduction semantics with Redex and you wish to give academic credit, please cite the book (above). If you are studying the effectiveness of meta-tools, the proper citation is our POPL 2012 paper.

 

至於那個

 v.7.2

2 Long Tutorial

This tutorial is derived from a week-long Redex summer school, run July 27–31, 2015 at the University of Utah.

2.1 The Theoretical Framework

Goals
— abstract syntax
— notions of reduction, substitution
— reductions and calculations
— semantics
— standard reduction
— abstract register machines
— types

The lambda calculus:

e = x | (\x.e) | (e e)

Terms vs trees, abstract over concrete syntax

Encode some forms of primitives: numbers, booleans – good for theory of computation; mostly irrelevant for PL. extensions with primitive data

e = x | (\x.e) | (e e) | tt | ff | (if e e e)

What we want: develop LC as a model of a PL. Because of history, this means two things: a simple logic for calculating with the terms of the language e == e’ and a system for determining the value of a program. The former is the calculus, the latter is thesemantics.

Both start with basic notions of reduction (axioms). They are just relation on terms:

 ((\x.e) e’) beta e[x=e’]

pronounced: e with x replaced by e’

 ((\x.e) e’) beta [e’/x]e

pronounced substitute e’ for x in e

Think substitution via tree surgery, preserving bindings

Here are two more, often done via external interpretation functions (δ)

(if tt e e’) if-tt e

(if ff e e’) if-ff e’

If this is supposed to be a theory of functions (and if expressions) we need to be able to use this relations in context

        e xyz e’
    ————–
        e  =  e’
    
        e = e’                 e = e’                 e = e’
    ————–         ————–         ————–
    e e” = e’ e”         e” e = e” e’          \x.e  = \x.e’
    
    plus reflexivity, symmetry, and transitivity
for any relation xyz

Now you have an equational system. what’s it good for? you can prove such facts as

e (Y e) = (Y e)

meaning every single term has a fixpoint

All of the above is mathematics but it is just that, mathematics. It might be considered theory of computation, but it is not theory of programming languages. But we can use these ideas to create a theory of programming languages. Plotkin’s 1974 TCS paper on call-by-name versus call-by-value shows how to create a theory of programming languages.

In addition, Plotkin’s paper also sketches several research programs, mostly on scaling up his ideas to the full spectrum of languages but also on the precise connection between by-value and by-name their relationship, both at the proof-theoretical level as well as at the model-theoretic level.

Here is Plotkin’s idea as a quasi-algorithm:
  1. Start from an abstract syntax, plus notions of scope and scope-preserving substitution. Consider closed terms Programs.
  2. Identify a subset of expressions as Values. Use v to range over Values.Note The complement of this set was (later) dubbed computations, due to Moggi’s work under Plotkin.
  3. Define basic notions of reduction (axioms). Examples:

    ((\x.e) e’) beta-name e[x=e’]

    ((\x.e) v) beta-value e[x=v]

  4. Inductively generate an equational theory from the basic notions of reduction.
  5. This theory defines a semantics, that is, a relation eval from programs to values:

    eval : Program x Value

    def e eval v iff e = v

  6. Prove that eval is a function, and you have got yourself a specification of an interpreter.

    eval : Program -> Value

    eval(e) = v

    Note This step often reuses a variant of the Church-Rosser theorem of the mathematical theory of lambda calculus.

  7. Prove that the calculus satisfies a Curry-Feys standard reduction property. This gives you a second semantics:

    eval-standard : Program -> Value

    def eval-standard(e) = v iff e standard reduces to v

    The new semantics is correct:

    Theorem eval-standard = eval

    Standard reduction is a strategy for the lambda calculus, that is, a function that picks the next reducible expression (called redex) to reduce. Plotkin specifically uses the leftmost-outermost strategy but others may work, too.

Plotkin also shows—on an ad hoc basis—that this evaluator function is equivalent to Landin’s evaluator based on the SECD machine, an abstract register machine.
Plotkin (following Morris, 1968) uses step 6 from above to add two ideas:
  • The interpreter of a programming language (non-constructively) generates a theory of equivalence on phrases.

    def e ~ e’ iff placing e and e’ into any context yields programs that produce the same observable behavior according to eval

    Theorem ~ is the coarsest equivalence theory and thus unique.

    Let’s call ~ the Truth.

  • Theorem e = e’ implies e ~ e’. Naturally the reverse doesn’t hold.
Matthias’s (post)dissertation research extends Plotkin’s work in two directions:
  1. Plotkin’s “algorithm” applies to imperative programming language, especially those extending the lambda calculus syntax with (variable) assignment and non-local control operators.Imperative Extensions explains how two of these work.
  2. It is possible to derive useful abstract register machines from the standard reduction semantics of the programming language
    Each machine M defines a new semantics:

    def eval-M(e) = v iff load M with e, run, unload, yields v

    For each of these functions, we can prove an equivalence theorem.

    Theorem eval-M = eval-standard = eval

His work also shows how this approach greatly simplifies proofs of consistency for the semantics of programming languages and especially so-called type soundness theorems.

 

未曾深研，不敢亂講呦。