标签：end programming Programming logical choice IncRe logic CTM semantics

目录

• 基础信息
• 9 Relational Programming
  • 9.1 The relational computation model
  • 9.2 Further examples
  • 9.3 Relation to logic programming
    • 9.3.2 Operational and logical semantics
    • 9.3.3 - 9.3.4
    • 9.3.5 Logic programming in other models

本篇前置：

• IncRe[3] CTM 2.1 Defining practical programming languages
  https://www.cnblogs.com/minor-second/p/15691517.html

基础信息

• 
• 书名：Concepts, Techniques, and Models of Computer Programming
• ISBN：978-0-262-22069-9
• 9 Relational Programming
• Incentive：本学期课程有一门“约束式编程”，是一种非常有意思的paradigm. 想弄明白其在各种programming paradigm全景中的位置。

9 Relational Programming

• 函数：一进一出。关系：没有明显进出方向，且可能一进，0至多个出

Conceptually, the choice statement nondeterministically picks one among a set of alternatives. During execution, the choice is implemented with search, which enumerates the possible answers. We call this “don’t know nondeterminism,” although the search algorithm is almost always deterministic

“任选一个可行解”，但没完全随机任选（因为搜索过程是确定性的）。称为“don't know nondeterminism”
Prolog核心就是这个choice
为什么说inefficient？如果你利用choice机制，强行用确定型图灵机模拟非确定型（不停地搜），那就指数爆了
用处：小搜索空间强行做。或者除了搜没有别的办法的时候。

9.1 The relational computation model

• choice语句，创建了choice point，可能失败了回溯回来（注，这并不是implement的唯一形式）
• fail语句：出现3=4这种时隐式执行，表示失败（之前是抛出异常）
  • 也可以显式执行fail

这是kernel language，需要参考IncRe[3]进行理解。
下面是一个例子。其中我们去http://mozart2.org/mozart-v1/doc-1.4.0/
可以找现成的求解包，即http://mozart2.org/mozart-v1/doc-1.4.0/system/node9.html#chapter.search

declare
fun {Soft} choice beige [] coral end end
declare
fun {Hard} choice mauve [] ochre end end
declare
proc {Contrast C1 C2}
 choice C1={Soft} C2={Hard} [] C1={Hard} C2={Soft} end
end
declare
proc {Suit X}
 Shirt Pants Socks
in
 {Contrast Shirt Pants}
 {Contrast Pants Socks}
 if Shirt==Socks then fail end
 X = suit(Shirt Pants Socks)
end
{Show {Search.base.all Suit}}

输出

[suit(beige mauve coral) suit(beige ochre coral) suit(coral mauve beige) suit(c\
oral ochre beige) suit(mauve beige ochre) suit(mauve coral ochre) suit(ochre be\
ige mauve) suit(ochre coral mauve)]

• 注意suit是record的label，而不是proc名字Suit
• proc和fun中有choice，所以其结果有“don't know nondeterminism”
  • proc中的choice就是可能选择一个语句序列去执行
• “约束”可以用choice表示，也可以fail“补充”上约束

When a fail is executed, execution “backs up” to the most recent choice statement, which picks its next alternative. If there are none, then the next most recent choice picks another alternative, and so forth.

由此，引出“搜索树”“回溯”等概念
encapsulated: inside a kind of "environment": 控制怎么搜，隔绝内外防止不确定性造成破坏。模块化，层次化
Solve在ExpRe[23]下载到的Oz中并没有实际实现。可以使用Search.base.all方法之类的代替，像之前的例子一样。

9.2 Further examples

一个例子

declare
fun {Digit}
choice 0 [] 1 [] 2 [] 3 [] 4 [] 5 [] 6 [] 7 [] 8 [] 9 end
end
declare
proc {Palindrome X}
X=(10*{Digit}+{Digit})*(10*{Digit}+{Digit})
(X>0)=true
(X>=1000)=true
(X div 1000) mod 10 = (X div 1) mod 10
(X div 100) mod 10 = (X div 10) mod 10
(X mod 8) = 5
end
{Show {Search.base.all Palindrome}}

可以看到，利用=，可以直接增加约束。
输出结果
[1221 1221 3773 5005 5445 5005 3773 5005 5005 5445]
关于constraint programming的一条看法

The resulting solution is not very efficient; for more efficiency we recommend using constraint programming instead, as explained in chapter 12. Using relational programming is a precursor of constraint programming

9.3 Relation to logic programming

The advantage of logic programming is that programs have two semantics, a logical and an operational semantics, which can be studied separately.

logical semantics非常简单，易于研究
有state的情况使用logical semantics就不方便了

• 举例：命题逻辑，一阶逻辑，带等词的一阶逻辑
  课本给出了带等词的一阶逻辑
  

A logical formula with no free identifier occurrences is called a logical sentence

本书此处不允许自由变元。必须“闭式”
relation vs. predicate：relation是predicate的模型
一个logical model的例子（针对带等词的，含有两条公理“父亲唯一”“父亲的父亲是爷爷”的系统）

Domain of discourse: {george, tom, bill}
Father relation: {father(george, tom), father(tom, bill)}
Grandfather relation: {grandfather(george, bill)}
Equality relation: {george = george, tom = tom, bill = bill}

logic programming组成要素：形式系统，query，theorem prover

i.e., a system that can perform deduction using the axioms in an attempt to prove or disprove the query. Performing deductions is called executing the logic program

logic programming一些问题：完全性（哥德尔不完备定理）、执行效率、"constructive"（需要实际给出结果）
解决方法：限定在小范围（比如Horn clause和resolution）。用一些具体领域的额外知识（如关于整数的知识）

9.3.2 Operational and logical semantics

There are two ways to look at a logic program: the logical view and the operational view. In the logical view, it is simply a statement of logic. In the operational view, it defines an execution on a computer.

relational program to logic:
我认为的核心有两点

• X=Y就是\(x=y\)，第二次赋值会报错（fail），区别于“stateful”
• choice被翻译成析取，带来了一对多“关系”，故第9章区别于第2章

等价的logical semantics不一定有相同的operational semantics. 写程序时先写前者，再写后者。两者的tension需要被权衡：

the logical semantics should be simple and the operational semantics should be efficient

一个例子：append

• 其有明确的operational semantics
• 也可以翻译成logical semantics: \(\forall a,b,c.append(a,b,c)\leftrightarrow (a=nil\wedge c=b)\vee(\exists x,a',c'.a=x|a'\wedge c=x| c'\wedge append(a',b,c'))\)
  • 其中竖杠是链表连接
• 反过来，也可以理解成先有了对append谓词的归纳定义（如上），再翻译成operational semantics
• 实际执行时，{Append [1 2 3] [4 5] x}，可以用logic理解成找到x使得\(append([1,2,3],[4,5],x)\)属于指定的关系（relation）。证明过程也就是logic program的执行（execute）过程
• 程序不完备：一些operational semantics不一定能找到logical semantics表达的全部解
  • 例子：某个operational semantics为了知道前两个求最后一个，而不是为了知道后两个求前一个。

9.3.3 - 9.3.4

解不唯一，需要不确定性和choice
还是append，还是一样的logical semantics，使用choice得到不确定的operational semantics
可能得到无限或者指数爆炸的结果，所以lazy非常重要。甚至有的时候搜无限的非法，找不到一个合法
所以尽量不用不确定性
和Prolog关系：relational computation model接近pure Prolog. Prolog有一些缺少logical semantics的operational semantics，但pure Prolog没有
relational computation model与Prolog区别：是否用Horn与resolution rule，是否支持高阶，是否显式写出不确定性等

9.3.5 Logic programming in other models

• 增加concurrency并发
• 简单的state使用仍不超出logic programming范畴（比如被encapsulated辅助operation，或者只做参数）
• constraint programming地位

It is the most powerful model in the sense that it has the most sophisticated mechanisms both for specifying and automatically determining the control flow. From the logic programming viewpoint, it has the strongest deduction abilities

标签：end,programming,Programming,logical,choice,IncRe,logic,CTM,semantics
来源： https://www.cnblogs.com/minor-second/p/15692707.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。