异国情调的编程思想
继续我们关于异类编程思想的系列文章，我们将探讨逻辑编程的主题以及一种称为数据记录的特殊形式。
数据日志由查询处理器执行，该处理器给出这两个输入，查找数据库和规则所隐含的事实的所有实例。对于我们的示例，我们将使用Souffle语言编写示例。语言的名称是系统的，本体的，未发现的事实发现逻辑引擎的缩写。可以使用以下命令将其简单地安装在许多Linux系统上：
Souffle是一种极简主义的数据记录系统，旨在处理大型数据集的复杂查询，例如在大型代码库上进行静态程序分析时遇到的查询。 Souffle是用C ++实现的，可以通过编译为C将数据日志程序编译为独立的可执行文件。它是迄今为止这些系统最简单，最高效的实现之一，尤其是它在逻辑引擎之上具有简单的类型系统。
Datalog编码一个可确定的逻辑片段，对于该逻辑片段，可以在有限的术语范围内直接计算满意度。这些术语包括三类表达。在句法上以句号后缀表示的事实。
用头和身体词表示的规则，其间有转门符号（\（\ vdash \））。
这些术语的一个例子是关于希腊哲学家苏格拉底的“古典”分类三段论。苏格拉底是一个人，所有人都是凡人，因此我们可以推断苏格拉底是凡人。
//所有的人都是凡人/ valar morghulis凡人（X）：-人（X）。 //苏格拉底是一个男人。人类（＆＃34; Socrates＆＃34;）。 //苏格拉底是凡人吗？ ？-凡人（＆＃34; Socrates＆＃34;）。
Souffle程序的执行实际上是通过规则的规定从输入事实到推导出的输出事实的一组转换。
Souffle可以从各种来源读取输入事实，包括stdin，CSV文件和SQLite数据库。默认输入源是用于关系的制表符分隔的文件，其中文件中的每一行代表该关系中的事实。这是通过表单的IO输入声明指定的。
这将从文件A中读取。制表符分隔值的事实表示符号值n。但是，我们可以通过向输入传递明确的IO参数来修改输入。
一个简单的端到端示例是通过简单的一对一映射将一组符号输入与一组数字输入相关联的程序。我们可以按照以下规则编写简单的A到B转换。
/ *来自A.facts的输入* /。 decl A（n：符号）。输入A / *输出到B.csv * /。 decl B（n：number）B（0）：-A（＆＃34; Hello＆＃34;）。 B（1）：-A（＆＃34; World＆＃34;）..输出B
这是从A.facts中的输入事实中读取的，并输出B.csv，当我们使用以下命令调用Souffle时，它的输出看起来并不奇怪。
数据日志内部的逻辑由关系指定，关系是与数量相关的类型化变量的有序元组。例如，如果我们有一组命名实体（表示为符号），则可以分配一个关系，该关系将一个属性映射为每个事实。
每个变量都有特定的类型，用var：type表示，其中type是以下内置函数之一。
关系可以采用多个参数，这些参数根据该关系上的规则将属性分配给符号集合。
这些关系的规则由条款定义。当一对（x，y）处于A关系中时，以下项可以被读取：
Souffle中的子句在逻辑上称为Horn子句。它们由子项组成，这些子项与表示语句\（u \）的连词（\（\ land \））（逻辑与）结合在一起。可以阅读以下数学语句：
以上称为隐含形式。从逻辑上讲，这等效于以析取（\（\ lor \））（在编程中为逻辑“或”）和否定（\（\ lnot \））（在编程中为逻辑非）编写的语句。
在子句中，联合表达式内部出现的自由变量是隐式通用量化的，即要求它们在域中保留变量的全部（表示为（（\ forall \））替换。
因此，举例来说，我们知道克林贡人和人类都在吃东西，但是显然，机器人们不会。我们在类型为symbol的变量项X上编写以下规则。
从给定的输入事实集合中，关于给定种类的符号，范围内的符号会产生以下输出。
术语也可以取反，例如，如果我们要枚举所有吃东西的军官，可以编写以下规则（不包括机器人）。
一个更复杂的规则可以由多个用命令分隔的术语组成，所有这些都必须评估为真。例如，如果两名军官的职级相同且不是同一个人，则他们是同级。我们使用中间变量Z来测试此关系中的等级相等。
规则也可以是递归的。例如，我们想要编写一个查询，该查询找到给定事实集的所有一级朋友关系，我们可以编写以下递归定义。
关系的重要类别是等价关系。这些是满足附加约束条件的两个术语之间的关系：自反性，对称性和可传递性。这种形式的关系的行为类似于在代数中如何处理等号。
\ [\ begin {align *} a＆amp; = a \\ a＆amp; = b \ Rightarrow b = a \\ a＆amp; = c，b = c \ Rightarrow a = c \ end {align *} \]
// R1的每个元素都等同于R2的每个元素。等于（x：number，y：number）等于（a，b）：-R（a），R（b）。 //自反性等效项（a，a）：-等效项（a，_）。 //对称当量（a，b）：-当量（b，a）。 //可传递性等价性（a，c）：-等价性（a，b），等价性（b，c）。
在关系的实现中，数据和中间推导存储在公共的B树数据结构中。但是，可以通过传递一个明确的参数来强制对此特定用例使用不相交集或trie数据结构来对此进行修改。
。 decl A（x：number，y：number）eqrel //不交集。 decl B（x：number，y：symbol）btree // B树。 decl C（x：number，y：symbol）brie //密集的特里
使用整数类型（数字，无符号和浮点型）时，算术表达式的行为符合预期，并且可以进行模式匹配。例如，我们可以将斐波那契函数写成就其本身而言的关系。
Souffle具有有限的类型系统，可用于跟踪在子句表达式中量化的变量类型。例如，不能有一个同时包含符号和无符号整数的变量。但是，我们可以在语言的基础类型之上定义自定义类型同义词，这将使我们在语义上区分不同的用户定义类型的符号和数字量。例如：
。输入Person＆lt ;:符号。键入食物＆lt ;：符号。 decl Eats（x：人，y：食物）。晚餐（x：人，y：食物）晚餐（x，y）：-吃（x，y）。 //键入正确的Dinner（x，y）：-Eats（y，x）。 //不好打字，人！=食物
只要同义词的基础类型是等效的，也允许类型同义词的并集。
。类型A＆lt ;:数字。 B型＆lt ;：数字。类型C = A | B //在A或B中
该语言还具有定义求和和乘积类型的能力，这使我们可以将选项和记录都作为子句中的术语。 。 类型Sum = A {x：number} | B {x：符号}。 输入Prod = C {x：数字，y：符号} 例如，我们可以从具有head元素和tail元素的产品类型中构建链接列表（或缺点列表）。 //链表。 类型列表= [头：数字，尾巴：列表]。 decl MyList（x：List）MyList（[1，[2，nil]]）。 逻辑编程是表达抽象程序语义的一种非常自然的方式，借助Souffle之类的工具，我们拥有出色的逻辑引擎，可以将其嵌入其他静态分析应用程序中，以收集有关代码的事实并推断出有关代码组成和用法的含义。 这项功能强大的技术和未来的静态分析工具将在将来产生全新的推理和综合代码的方式。
