Lustre/Scade 形式化语义基础 —— 同步Kahn网络 (1996)
在<同步反应式系统>课程中，提到了Lustre语言的理论来自ICFP’96。下面将介绍 ICFP’96 Synchronous Kahn Network 的内容。
数据流式编程一直是处理反应式系统（如自动控制、信号处理）的重要范式。而同步 Kahn 网络（Synchronous Kahn Networks）作为一种融合了 Kahn 进程网络、同步数据流编程和函数式编程优势的技术，自 1996 年在 ICFP 会议上被提出以来，经过多年发展，已在工业界得到一定应用。
诞生背景
数据流式编程的发展脉络
在20世纪70年代，Lucid 语言就作为一种为函数式语言提供基于流的语言被提出。与此同时，Kahn 证明了异步确定性进程网络的语义可以用流上的递归方程组来描述，这与Lucid程序非常相似。随后，lazy evaluation概念出现，使得处理有限和无限的数据结构成为可能，像LML和Haskell 这样的现代惰性函数式语言也能轻松编写数据流程序。
但这些惰性函数式语言编写的程序有时效率较低，Wadler 提出了 listlessness技术，后来又推广为 deforestation技术，旨在避免在列表程序中构建中间列表，以提高效率。
另一方面，自动控制和信号处理工程师面临着从模拟设备向顺序计算机过渡的问题。他们一直使用流上的递归方程组作为推理系统的自然形式，但将这些方程转换为顺序程序既繁琐又容易出错。于是，像 LUSTRE、SIGNAL 这样的语言，PTOLEMY 这样的工具箱以及相关编译器应运而生，它们被称为 Synchronous Data-flow，属于同步编程家族，而 ESTEREL是该家族中最具代表性的成员。
同步Kahn网络的提出
当时的同步数据流语言虽然在反应式系统领域取得了成功，但存在诸多限制，比如不允许函数的递归定义。这是因为反应式系统需要持续与环境交互，为保证安全交互，其反应必须使用有界内存和有界反应时间。
然而，研究者们发现，同步操作语义和时钟约束规则并不局限于这些反应式限制，它们可以应用于更通用的流语言，支持抽象、应用和通用递归。于是，同步Kahn网络应运而生，它旨在扩展静态同步数据流的范围，将高阶和动态网络纳入其中，赋予更广泛的同步数据流网络意义。
同时，当时的去森林化技术在处理一些简单的同步程序时存在缺陷，比如在处理current v (x when c) c这类在LUSTRE中很容易被接受的程序时会出现发散情况，而且无法静态拒绝一些会导致无界FIFO执行的程序。同步Kahn网络的提出也正是为了解决这些问题，通过时钟演算来静态检查程序，确保程序能同步执行。
同步Kahn网络原理：从语言到编译
同步Kahn网络有着一套理论体系和技术方法，涵盖了专用的数据流语言、同步操作语义、时钟演算以及编译方法，这些共同构成了其原理。
同步Kahn网络的数据流语言
同步Kahn网络基于一种类似LUSTRE的语言构建，该语言是纯函数式同步反应数据流语言，但在一些方面与LUSTRE有所不同。
它的基本原语构建更加通用，能够轻松表达LUSTRE的原语。比如，const原语可以将标量常量转换为无限常量流，const i = i : const i，像const true就是一个无限的[true; true; ...]流；extend原语允许将函数流应用于数据流，extend (f:fs) (X:XS) = (f x) : (extend fs XS)，利用它可以定义像notl x = extend (const not) x这样的反相器和andl y = extend (extend (const and) x) y这样的与门，它们能对输入流进行逐点操作。
还有fby算符，也就是延迟操作符，(x :xs)fby y=x:y，它能安全地构建递归表达式（反馈网络或电路）而不会出现死锁，例如half = (const false) fby (notl half)就具有[false; true; false; true; ...]这样的无限周期性行为。当fby的第一个参数是常量流时，还可以使用更简单的pre函数，pre sx=s:x，上述half也可写成half = pre false (notl half)。
此外，when原语能从流中提取子流，(x : XS) when (true : Cs) = x : (XS When CS)，(x:XS) when (false : Cs) = xs when cs；merge原语则可以从子流构建流，merge (true:cs) (X:XS) y = x: (merge cs xs y)，merge (false:cs) x (y:ys) = y: (merge cs x ys)。
该语言还采用了curry化，并且其时钟演算更具一般性，允许时钟被推导出来，这得益于与经典类型推断的类比，有助于将其扩展到函数式特性。
同步操作语义
程序在上述语言中可以以按需求调用的方式执行，但这种方式像处理列表一样，会导致中间结构被分配然后由垃圾回收器回收，效率低下。而同步 Kahn网络的同步操作语义则是经典惰性语义的受限关系，不允许某些归约规则，使得大量程序能以同步方式执行，在执行过程中不管理列表。
同步操作语义通过转换关系σ ⊢ e ⟶ e'来定义，意思是在环境σ中，表达式e的一个执行步骤产生值v并变成表达式e'。环境σ的形式为[x₁ ⟶ y₁, ..., xₙ ⟶ yₙ]，其中xᵢ和yᵢ表示变量名，v要么是标量表达式e，要么是空。
以const原语为例，它产生一个常量列表，const v程序的一个执行步骤产生v，并继续为const v。如果没有操作等待其值，它可能不产生任何东西，这种情况被称为空规则。extend原语逐点将标量函数列表应用于参数列表，其语义规定两个参数必须同时存在或不存在；如果都不存在，代码保持不变且不产生值。这体现了同步语义的关键特点，即不考虑参数产生值和不产生值的所有组合情况，只考虑部分情况，避免了仅一个参数存在时对表达式的求值，也不允许在临时列表中存储中间结果，这与经典操作语义有很大区别。
类似地，merge原语在同步语义下只考虑三种情况，而不是所有八种可能情况；fby只有在第一个参数产生值时才可能产生值，并且此时会转换为pre操作；pre操作符在操作上类似于锁存器，它将记录的值输出并存储输入。
对于递归表达式，需要区分rec应用于基本表达式和函数表达式的情况。在反应式数据流中，只允许rec x₀. e₀这样的不动点，前提是x₀在e₀中不是自由的，否则会被视为死锁。而同步Kahn网络扩展后，能够处理更一般的递归情况。
时钟演算
时钟演算的目标是提供可静态检查的条件，确保表达式能够同步求值。它是对之前相关工作的推广，采用推断时钟的方式，并使用unification而非不动点，同时还扩展到了函数式表达式。
时钟演算的判断形式为H ⊢ e : cl，表示在环境H中，表达式e具有时钟cl。环境H是关于e的自由变量时钟的假设列表，形式为[x₀: cl₀, ..., xₙ: clₙ]。时钟cl可以是时钟变量α、由布尔流表达式e监控的子时钟cl one，或者是时钟函数cl ⟶ cl。
时钟系统的设计借鉴了经典的Damas-Milner类型系统，只是对递归规则做了轻微修改。常量表达式可以匹配任何时钟，因此具有多态时钟∀α. α；extend的两个参数必须具有相同的时钟；when表达式的时钟取决于第二个参数的值，通过on结构来表示；merge e₁ e₂ e₃表达式要符合时钟要求，e₂的时钟需是e₁为真时的受限时钟，e₃的时钟需是e₁为假时的受限时钟；fby表达式的两个参数时钟要么相同，要么第一个参数的时钟比第二个快；pre表达式保持其参数的时钟。
在对流传变量进行抽象时，必须跟踪被抽象的变量，因为它可能出现在时钟表达式中。应用规则与抽象规则保持一致，标量变量的抽象和应用不会改变时钟。
时钟演算的一个重要定理是可靠性定理：对于所有表达式e和时钟cl，如果⊢ e : cl，那么存在v、e'和cl'，使得⊢ e ⟶ e'且⊢ e' : cl'。这意味着能够被时钟化的表达式可以进行同步执行步骤，并且执行后得到的表达式仍然是可时钟化的，保证了同步执行的持续进行。
编译方法
同步Kahn网络的编译目标是将符合时钟要求的流程序转换为标量上的转换函数。初始程序需要以按需求调用的方式执行，而最终程序将以按值调用的方式执行。
编译过程基于同步操作语义，程序e的一般执行过程为e = e₀ ⟶ e₁ ⟶ e₂ ⟶ ...，表示e₀的一个执行步骤产生值v₀并转换为e₁，以此类推。编译的目的就是生成一个转换函数，该函数的迭代将产生连续的值vₜ。这个转换函数可以分解为两部分：产生标量输出vₜ的代码函数，以及修改机器内部内存的modif-state函数，以体现eₜ变为eₜ₊₁的过程。
编译关系定义为σ ⊨ e : <c, m, s>，表示在环境σ中编译表达式e产生代码c、修改内存的指令序列m和初始内存s。环境σ的形式为[x₁: <c₁, m₁, s₁>, ..., xₙ: <cₙ, mₙ, sₙ>]，内存表达式可以是空内存、内存名、名称与内存或标量值的链接集合、递归内存或内存函数。
不同原语的编译规则遵循其语义规则。例如，const的编译代码部分返回其参数的值，modif-state部分是空指令，因为const机器不需要内部状态；merge的编译产生一个简单的if语句，modif-state指令来自merge的三个部分，内存部分是三个参数内存的并集；pre操作符在操作上类似锁存器，编译时通过一个变量来实现，代码部分返回该变量的内容，modif-state部分在c产生值时计算该变量的新值，内存部分是其参数内存加上新的链接。
通过这样的编译方法，可以将同步Kahn网络的程序转换为高效的可执行代码，例如转换为CamL light语言代码，再进一步转换为C代码以获得更高的执行效率。