将语义分析用于调试器的演示性代码
zhang3
跑题加人身攻击了）
有进一步兴趣的可以去看相关内容
我的日记：
http://www.douban.com/note/103235092/
这个是民科挡箭牌，区段时序逻辑（Interval temporal logic ）
http://www.tech.dmu.ac.uk/STRL/ITL/itlhomepagese6.html#x7-70006.1
模拟这样一个顺序运行的程序：
c1: x=0;
c2: x=x+1;
c3: x=x+2;
%先各自表达一下这三个语句的语义：
c3的语义：
after(c3,value(x,V)):-before(c3,value(x,V1)),V is V1+2.
如果在c3运行之前，x的值是V1，那么在c3运行之后，x的值就是V1+2
c2的语义：
after(c2,value(x,V)):-before(c2,value(x,V1)),V is V1+1.
如果在c2运行之前，x的值是v1，那么在c2运行之后，x的值就是V1+1
c1的语义：
after(c1,value(x,0)).
c1运行之后，x的值是0（不管前面x是什么值）
%接下来要表达一下代码的顺序：c1->c2->c3
before(c3,X) :- after(c2,X).
before(c2,X) :- after(c1,X).
含义是：
在c3之前就是在c2之后。
在c2之前就是在c1之后。
%现在要开始查询了：
查询1：在语句c3运行之后，x的值是多少？
?- after(c3,value(x,V))
V=3
查询2：在语句c3运行之前，x的值是多少？
?- before(c3,value(x,V))
V=1
查询3：在语句c2运行之后，x的值是多少？
?- after(c2,value(x,V))
V=1
以上代码在swi-prolog中运行。
虽然是有点惨兮兮的，但是我们手工写进去的语义：
after(c3,value(x,V)):-before(c3,value(x,V1)),V is V1+2.
after(c2,value(x,V)):-before(c2,value(x,V1)),V is V1+1.
after(c1,value(x,0)).
和代码的顺序：
before(c3,X) :- after(c2,X).
before(c2,X) :- after(c1,X).
通过宏的方式写出，就可以和传统的程序一样了：
x=0;
x=x+1;
x=x+2;
这里的查询相当于设置了断点，然后查看变量的状态，区别就在，程序并没有真正的运行，而是通过逻辑推导，得到了这个断点时刻的变量状态。
？- after(C,value(x,3)).
C=c3
这个是问在哪个代码运行之后x的值会等于3
？- after(C,value(X,1)). %注意这个是大写的X哦。
C=c2
X=x
这个查询要查询两个变项，意思是问，在某个语句运行之后某个变量的值会等于1，请问这个语句是哪个，这个变量叫什么名字？
还有更复杂的组合查询
?- after(C,value(X,V)),V<2.
C = c2
X = x
V = 1 ;
C = c1
X = x
V = 0 ;
这个查询的含义是，在某个语句之后某个变量的值小于2，请问这些语句是什么，这个变量叫什么名字，变量的值分别是多少。
以上查询也都可以在swi-prolog上实际的运行。
一个阶段性目标：简单c语言的调试器
1 读入c语言写成的代码。
2 提供多种查询方法。
这种调试方法，远远超过现有的调试器的能力，因为它的视角，是上帝的视角，根据c语言代码所建立起来的逻辑数据库，包括了这个程序运行到任何时刻的信
息，因而你可以用逻辑查询的方式，查询关于这个程序的任何信息，其中一些查询方法在调试复杂算法时就显得很有用了。
可以进行诸如这样的查询：
列出x的值等于104的时候，对y进行赋值操作的语句。
代码用来计算数组之和所用到的时间总和是多少？
列出在某个循环中，x的值的所有变化，以及对应的y值。
这种方法已经完全抛开了现有的编译器，解释器的构造原理，通过完整的语义分析，而不是通过实际或模拟运行，对简单c语言进行各个层次的调试，直接得到我
们需要通过查询要找到的信息。
zhang3
liuxinyu
Good to have this kind of topic.
不知道你有没有听说过``Numerical representation''
WIKIPEDIA上没有这个词条，最接近的是positional numeral system。
http://en.wikipedia.org/wiki/Positional_numeral_system
Donald Knuth在TAOCP中有说过这个。简单起见，我们看下面一对代码段：
懂Haskell的我们看这个：
代码A
data List a = NIL | Cons a (List a)
tail (Cons x xs) = xs
append NIL ys = ys
append (Cons x xs) ys = Cons x (append xs ys)
代码B
data Nat = Zero | Succ Nat
pred (Succ n) = n
plus Zero n = n
plus (Succ m) n = Succ (plus m n)
不懂Haskell，但是懂C++ template meta programming的看这个：
代码A:
struct NIL;
template<class T, class U> struct List{
typedef T Head;
typedef U Tail;
};
template<class L> struct Tail;
template<class T, class U> struct Tail<List<T, U> >{
typedef U Result;
};
template<class L, class X> struct Append;
template<class X> struct Append<NIL> {
typedef List<X, NIL> Result;
};
template<class X, class T, class U> struct Append<List<T, U> >{
typedef List<T, typename Append<U, X>::Result> Result;
};
代码B:
struct Zero;
template<class N> struct Succ{
typedef N Result;
}
template<class N> struct Pred;
template<class N> struct Pred<Succ N>{ typedef N Result; };
template<class N, class M> struct Plus;
template<class N> struct Plus<Zero, N>{ typedef N Result; };
template<class N, class M> struct Plus<Succ<N>, M>{
typedef Succ<typename Plus<N, M>::Result> Result;
};
懂Prolog的可以参考上面的post。
其实Numerial representation远远不止这个看似皮毛的东西，另外一个典型的例子是Binomial Heap，任何一个自然数都
对应一个Binomial Heap。
有兴趣的可以参见Chris Okasaki的著作``Purely Functional Data structures''的第9章。
另外:C++的那个可以参见我2006年的post [1]，以及2007年的[2],[3]
--
Liu
[1]. http://sites.google.com/site/liuxinyu95/softdev.books.book1.essay7.chn
[2]. http://sites.google.com/site/liuxinyu95/softdev.books.book2007.essay1.chn
[3]. http://sites.google.com/site/liuxinyu95/softdev.books.book2007.essay2.chn
liuxinyu
Sorry, 有些跑题，只是我看了Prolog的那段定义后，立即和Numerial representation的topic碰撞了一下：）
--
LIU
> [2].http://sites.google.com/site/liuxinyu95/softdev.books.book2007.essay1...
> [3].http://sites.google.com/site/liuxinyu95/softdev.books.book2007.essay2...
机械唯物主义 : linjunhalida
上面看起来是把一个延迟求值的, 状态机随时间改变的状态信息流.
有个问题: 顺序求值下面, 前一个语句状态映射到后一个语句执行的状态的函数往往不是可逆的..根据状态好像推不到前个状态?
还有就是即使用动态规划, 这样推导是不是会很慢? 毕竟实际程序是利用内存空间, 这个状态就大了.
突然间, 想起群论的概念..不过就扯远了..
2010/11/30 zhang3 <open...@gmail.com>:
zhang3
1 状态空间很大
这个要通过对逻辑系统本身的优化来做。有些查询会产生组合爆炸，这个问题的解决方案是，1，内存不够直接当掉。2 逻辑系统本身的自省机制。
2 不可逆运算
毕竟是演示性的，推导可以从前往后也可以从后往前。
这两个问题都要通过对逻辑系统的优化和改进来做，转化为逻辑问题的好处是，可以公理化。
On 11月30日, 下午3时27分, 机械唯物主义 : linjunhalida <linjunhal...@gmail.com>
wrote:
> 有点SICP里面介绍过的, 看事物的2个角度: 对象和流.
> 上面看起来是把一个延迟求值的, 状态机随时间改变的状态信息流.
> 有个问题: 顺序求值下面, 前一个语句状态映射到后一个语句执行的状态的函数往往不是可逆的..根据状态好像推不到前个状态?
> 还有就是即使用动态规划, 这样推导是不是会很慢? 毕竟实际程序是利用内存空间, 这个状态就大了.
> 突然间, 想起群论的概念..不过就扯远了..
>
> 2010/11/30 zhang3 <openau...@gmail.com>:
liuxinyu
SICP里还提到了:non-determined computing:
http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-28.html#%_idx_4876
另外这一章：
http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-24.html#%_sec_3.5
里注意一下那些信号流图。
本质上如果是一一映射的函数y=f(x)，那么已知y是可以推导x的。但是更多的情况下这个不成立，
会存在x1,x2, ..., 都满足y=f(xi)。如果这个空间是有限的，还存在利用non-determined computer解的可能。
实际上，应用程序的复杂度会急速膨胀，超出我们能够忍受的范围。
其实，一段程序，可以抽象成一个有限状态机(finite state machine)，程序运行的过程，就是状态转换的过程。
但是试图搞正确性证明，或者分析就成了世界级的难题。
好几年前粗略了看了下哥德尔不完全性定理，和希尔伯特第十问题。感觉挺悲观的。
不过还只支持这方面的尝试，无论如何，一些结论和劳动成果能极大的改善现有的调试和分析手段。
--
LIU
On Nov 30, 3:27 pm, 机械唯物主义 : linjunhalida <linjunhal...@gmail.com>
wrote:
> 有点SICP里面介绍过的, 看事物的2个角度: 对象和流.
> 上面看起来是把一个延迟求值的, 状态机随时间改变的状态信息流.
> 有个问题: 顺序求值下面, 前一个语句状态映射到后一个语句执行的状态的函数往往不是可逆的..根据状态好像推不到前个状态?
> 还有就是即使用动态规划, 这样推导是不是会很慢? 毕竟实际程序是利用内存空间, 这个状态就大了.
> 突然间, 想起群论的概念..不过就扯远了..
>
> 2010/11/30 zhang3 <openau...@gmail.com>:
open audio
如何让自然语言中的句式在程序语言中成为可能。
这个主题，是关于为世界的状态迁移建立逻辑模型的公理化方法。在这个方法下，赋值本身是一个动作，同时也产生一个事件。学术领域最接近的内容就是这个interval temporal logic。
全部的分析是不可能的，停机问题本身就绕不过去，但是不表示工业领域不能应用这些成果，至少可以论证，满足某些语义限制的代码，停机问题是有解的，事实上，我猜想：适当的限制输入集合，日常用到的不那么变态的程序，停机问题都是有解的。
liuxinyu
On Nov 30, 3:51 pm, open audio <openau...@gmail.com> wrote:
> 我所做的所有尝试都是围绕这样一个主题：
>
> 如何让自然语言中的句式在程序语言中成为可能。
>
> 这个主题，是关于为世界的状态迁移建立逻辑模型的公理化方法。在这个方法下，赋值本身是一个动作，同时也产生一个事件。学术领域最接近的内容就是这个interval
> temporal logic。
>
> 全部的分析是不可能的，停机问题本身就绕不过去，但是不表示工业领域不能应用这些成果，至少可以论证，满足某些语义限制的代码，停机问题是有解的，事实上，我猜想：适当的限制输入集合，日常用到的不那么变态的程序，停机问题都是有解的。
>
open audio
1 确定的输入
2 确定的运行过程
3 逻辑推理从前往后（不可逆也没关系，完全是按照计算顺序来的）
在这样的系统中，我们可做的查询就已经很丰富了，因为能推理出这一次程序运行过程中所有的状态。
（笨方法是用虚拟机跑一次，然后把中间状态全部记录下来，当然这是不可能的）
于是，程序员就可以用很多逻辑查询方式，在这一坨庞大的逻辑数据库中进行各种查询，直接去看自己关心的内容，而
不需要一遍又一遍的跑程序，琢磨代码。
要做更困难的事情，例如对不确定的输入，预测程序行为，这个有时候是可以做到的，但有时候是做不到的。
open audio
前面提到动态规划，这个东西的确和动态规划相关度挺高的。这里有一个例子，可以说明如何使用这种方法简化动态规划的编程，这里已经不是在调试了，而是使用这种形式做为编程语言了。
生产计划问题：
问题描述
工厂生产某种产品，每单位(千件)的成本为1(千元)，每次开工的固定成本为3(千元)，工厂每季度的最大生产能力为6(千件)。经调查，市 场对该产品的需求量第一、二、三、四季度分别为 2，3，2，4(千件)。如果工厂在第一、二季度将全年的需求都生产出来，自然可以降低成本(少付固定成本费)，但是对于第三、四季度才能上市的产品需付 存储费，每季每千件的存储费为0.5(千元)。还规定年初和年末这种产品均无库存。试制订一个生产计划，即安排每个季度的产量，使一年的总费用(生产成本 和存储费)最少。
使用动态规划理论就要建立数学方程，然后进行求解，写出来的程序也完全脱离了上述自然语言所描绘的形式。
人的思维从前往后是很容易的，所以我们可以先写这样一个函数P，这个函数输入每个季度的产量，然后计算出全年所需要的总费用：
total = P(V1,V2,V3,V4).
这个函数的实现代码，和题目中的自然语言几乎一样，通顺自然，而且自然的方式是命令式的，总费用做为一个状态不断累加上去。
然后对这个函数进行语义查询，方法是，在V1,V2，V3，V4组成的状态空间中进行搜索，得到让total为最小的这个组合。
这个语义查询，恰恰是和问题对应的：
试制订一个生产计划，即安排每个季度的产量，使一年的总费用(生产成本和存储费)最少。
通过这样的编程方法，我们就能让很多问题变得像自然语言描述那样通顺自然，符合人的思维方式。
liuxinyu
这不能不让人想起上世纪七十年代到八十年代讨论过的专家系统，还有逻辑式编程以及在马赛诞生的prolog。
希望用简单自然的语言描述问题一直是人们追求的方向。目前非常热的DSL也是某种意义上的这种努力。
但是客观存在的难题是，自然语言对问题的描述，并非是对问题的解。并且有些问题的逆问题，是公认的世界难题。
（举一个有趣的逆问题例子：CT成像）
就目前的成果看，性能和普遍性仍然是瓶颈。
人们还仅仅停留在使用这类方法（包括语言，和工具）进行prototyping的阶段上。一旦做好prototyping找到
解的方向（或者方法）后，人们往往倾向于使用其他工具进行有针对性的优化实现。
--
LIU