我有一个表示谓词逻辑公式的标准数据类型.表示析出的自然演绎消除规则的函数可能如下所示:
d_el p q =
if p =: (Dis r s) && q =: (Neg r) then Just s else
if q =: (Dis r s) && p =: (Neg r) then Just s else
Nothing where r,s free
x =: y = (x =:= y) == success
在统一失败时,该函数不返回Nothing,而是返回以下解决方案PACKS:
logic> d_el (Dis Bot Top) (Not Bot)
Result: Just Top
More Solutions? [Y(es)/n(o)/a(ll)] n
logic> d_el (Dis Bot Top) (Not Top)
No more solutions.
我错过了什么,为什么在统一失败时不el评价Nothing？
我是Haskell和编程的新手.关于在模式匹配的递归函数中绑定的问题.例如,假设我有一个函数来检查给定列表(x:xs)是否是另一个列表的子列表(y:ys).根据我的教科书中的例子,我最初的想法是:
sublist [] ys = True
sublist xs [] = False
sublist (x:xs) (y:ys)
| x == y = sublist xs ys
| x /= y = sublist (x:xs) ys
这适用于测试数据,例如,
sublist [1, 2, 3] [1, 2, 4, 1, 2, 3]
在哪里,我预计它会失败.我希望它会失败,因为
sublist [1, 2, 3] [1, 2, 4, 1, 2, 3]
= sublist [2, 3] [2, 4, 1, 2, 3]
= sublist [3] [4, 1, 2, 3]
在这一点上,我认为,[3] = 3:[]将与子列表中的(x:xs)匹配,[4,1,2,3]将与子列表中的(y:ys)匹配.那么子列表是如何工作的呢？
编辑:感谢大家,我想我已经解决了我的问题.如上所述,我("下意识地")想要子列表为我回溯.使用最后一个答案(BMeph)作为指南,我决定以不同的方式解决问题,以解决"绑定问题",即"回溯"问题.
subseq :: (Eq …我正在将无上下文语法转换为Greibach Normal Form(GNF).主要转换(来自Hopcroft和Ullman)是对语法的索引变量的迭代序列.它本质上是"无国籍的".我已经将它实现为适当索引的一系列折叠(实现相当简单):
gnf :: Ord a => Set (Rule a) -> Set (Rule a)
gnf rl = foldl step1 rl [1..maxIndex rl]
where step1 rl' k = foldl step2 rl' [1..k - 1]
where step2 rl'' j = noLR k (subst rl'' k j)
maxIndex rl返回一组规则中的最大变量索引; subst rl kj通过右侧以j -indexed变量开头的规则对k- indexed规则执行替换.执行gnf后,我需要以相反的顺序对语法执行最后一次传递.
问题是noLR,它使用左递归k - indexed规则转换语法.这是一个"状态"功能,因为唯一的变量必须为每个规则(或生成ķ -indexed规则),其noLR被应用.所以我写了一个有状态函数
noLR :: Ord a => Int -> Set (Rule a) -> State …在Haskell中处理相当大的代数数据类型时,有一种特殊的递归遍历没有通过折叠数据类型来捕获.例如,假设我有一个简单的数据类型表示命题逻辑中的公式,并在其上定义了一个折叠:
type FAlgebra ? ? =
(?, ?, -- False, True
? -> ?, -- Atom
? -> ?, -- Negation
? -> ? -> ?, -- Conjunction
? -> ? -> ?, -- Disjunction
? -> ? -> ?, -- Implication
? -> ? -> ?) -- Bi-implication
fold :: FAlgebra ? ? -> Form ? -> ?
fold (f,t,lit,not,con,dis,imp,iff) = fold' where
fold' (Fls) = f
fold' (Tru) = t
fold' (Lit ?) = lit ?
fold' (Not …在Brzozowski的"正则表达式的导数"和其他地方,如果R可以为空,函数δ(R)返回λ,否则,包括如下条款:
?(R1 + R2) = ?(R1) + ?(R2)
?(R1 · R2) = ?(R1) ? ?(R2)
显然,如果R1和R2都可以为空,则(R1·R2)可以为空,如果R1或R2可以为空,那么(R1 + R2)可以为空.然而,我不清楚上述条款应该是什么意思.我的第一个想法,映射(+),(·)或布尔运算到常规集是没有意义的,因为在基本情况下,
?(a) = ? (for all a ? ?)
?(?) = ?
?(?) = ?
并且λ不是一个集合(也不是设置δ的返回类型,这是一个正则表达式).此外,没有指出这种映射,并且有一个单独的表示法.我理解可空性,但我对δ的定义中的和,乘积和布尔运算的定义感到迷失:例如,在定义中,λ或how是如何从δ(R1)∧δ(R2)返回的关δ(R1·R2)？
编辑:解决了.我不知道在源文件中启用语言扩展没有在GHCi中启用语言扩展.解决方案是:set FlexibleContexts在GHCi中.
我最近发现Haskell中的类和实例中的类型声明是Horn子句.因此,我将The Art of Prolog,第3章中的算术运算编码为Haskell.例如:
fac(0,s(0)).
fac(s(N),F) :- fac(N,X), mult(s(N),X,F).
class Fac x y | x -> y
instance Fac Z (S Z)
instance (Fac n x, Mult (S n) x f) => Fac (S n) f
pow(s(X),0,0) :- nat(X).
pow(0,s(X),s(0)) :- nat(X).
pow(s(N),X,Y) :- pow(N,X,Z), mult(Z,X,Y).
class Pow x y z | x y -> z
instance (N n) => Pow (S n) Z Z
instance (N n) => Pow Z (S n) …编辑2:暗示de Bruijn指数可能更容易使用,我已经重新拟定了公式的大部分内部表示,以使用混合de Bruijn表示ala Connor McBride的论文.这极大地简化了一些关于语法的算法,这些算法必须处理 - 等效性,但使其他算法更加复杂.在任何情况下,这意味着自由变量可以标准化,绑定变量具有由其绑定距离表示的规范名称.这并不完全令人满意,但它至少是一个更好的开始.
编辑1:我意识到问题约束不足以保证变量的标准化.特别是,量词的迭代意味着必须首先将绑定器中的变量区分开来.因此,可能无法转义需要在每个抽象语法树上进行多次传递的解决方案.使用de Bruijn指数的建议通常是一个相当不错的解决方案,但是如果不打破符号及其实用性,它将不会轻易地给出标准化.
original: 设V是由自然数索引的无限变量集,fv(？)表示？的自由变量,而bv(？)表示任何一阶公式的？的绑定变量？我试图解决的问题如下.
让？和？是一阶公式.找到替换？1和？2使得:(a)fv(？1(？)),fv(？2(？)),bv(？1(？))和bv(？2(？))是不相交的; (b)fv(？1(？)),fv(？2(？)),bv(？1(？))和bv(？2(？))的并集与a的初始段同构.自然数; (c)bv中的所有变量(？1(？))小于bv中的所有变量(？2(？))小于fv中的所有变量(？1(？))小于fv中的所有变量(？2(？)).
困难在于公式中的绑定和自由变量的集合不一定是不相交的,并且可以迭代量词,意味着天真替换产生意外变量捕获,等等. …
给定两种非常规语言，它们的联合是正规的吗？
另外，为什么 L = L 1？L 2 = {a i b j | i,j >= 0} L 1 = {a i b j | 的并集 i >= j} 和 L 2 = {a i b j | 我<j}？
那么，L 1 = {a i b j |的并集是什么？i > j} 并且 L 2 = {a i b j | 我<j}？
我在使用这种setoid_rewrite策略进行重写时遇到了问题.在下面的实例声明中,我希望setoid_rewrite fmapComp将重写fmap iso ? fmap inv为fmap (iso ? inv).然而,Coq报告称在重写过程中"没有取得任何进展":
Instance functorsPreserveIsomorphisms
`{C : Cat o ?} `{D : Cat u ?}
{a b : o} {? : o ? u} (F : Functor C D ?) (I : a ? b) : ? a ? ? b.
Proof.
apply (Build_Isomorphism _ _ _ (? a) (? b) (fmap iso) (fmap inv)).
o : Type
? : o ? o ? Type
C …编辑:我应该说我目前如何解决这个问题.我定义了一个表示排列相等的原则,
Lemma permInd : ? (U : Type) (A : Ensemble U) (? ? : Perm A),
? ? = ? ? ? ? ? = ? ? ? ? = ?
然后在下面给我带来麻烦的证明语境中应用引理,并表明eta等价项是相等的.因此,当术语嵌套在记录中时,问题似乎显示出等效性.但我不擅长处理记录,所以我可能会遗漏一些东西.
原版的:
我无法证明嵌套在记录字段中的eta等价术语是否相等.作为参考,eta-reduction可以通过反身性独立证明:
Lemma etaEquivalence : ? (A B : Type) (f : A ? B), (? x : A, f x) = f.
Proof. reflexivity. Qed.
在我目前的证据背景下,我有两个必须证明相同的记录.完全破坏和展开,证明上下文和当前子目标看起来像这样:
U : Type
A : Ensemble U
perm0 : U ? U
pinv0 : U ? U
permutes0 : …