Mat*_*hid 11 logic haskell lambda-calculus logic-programming
我有一个有趣的问题,但我不确定如何用它来表达...
考虑lambda演算.对于给定的lambda表达式,有几种可能的缩减顺序.但其中一些不会终止,而另一些则会终止.
在lambda演算中,事实证明存在一个特定的减少顺序,如果实际存在,则保证总是以不可简化的解决方案终止.它被称为正常秩序.
我写了一个简单的逻辑解算器.但麻烦的是,它处理约束的顺序似乎对它是否找到任何解决方案产生了巨大影响.基本上,我想知道我的逻辑编程语言是否存在类似正常顺序的东西.(或者说,单纯的机器无法确定地解决这个问题.)
这就是我所追求的.据推测,答案关键取决于"简单逻辑解算器"到底是什么.所以我将尝试简要描述一下.
我的节目紧密地基于编程乐趣(Jeremy Gibbons&Oege de Moor)第9章中的组合系统.该语言具有以下结构:
求解器的输入是单个谓词.谓词可能涉及变量.求解器的输出为零或更多解.解决方案是一组变量赋值,它使谓词成为正确.
变量持有表达式.表达式是整数,变量名或子表达式的元组.
有一个等式谓词,用于比较表达式(不是谓词)的相等性.如果用其值替换每个(绑定)变量使两个表达式相同,则会感到满意.(特别是,每个变量都等于它自己,绑定与否.)这个谓词是使用统一来解决的.
还有AND和OR的运算符,它们以明显的方式工作.没有NOT运算符.
有一个"存在"运算符,它基本上创建局部变量.
定义命名谓词的工具支持递归循环.
关于逻辑编程的一个"有趣的事情"是,一旦你编写了一个命名谓词,它通常会向前和向后(有时甚至是横向).典型示例:用于连接两个列表的谓词也可用于将列表拆分为所有可能的对.
但有时向后运行谓词会导致无限搜索,除非您重新排列术语的顺序.(例如,交换一个AND的LHS和RHS或者一些OR.)我想知道是否有一些自动方法来检测运行谓词的最佳顺序,以确保在解决方案集完全正确的所有情况下立即终止有限.
有什么建议？
| 归档时间： |
|
| 查看次数： |
286 次 |
| 最近记录： |