dan*_*tin 5 algorithm variables performance formula substitution
编辑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(？)).
困难在于公式中的绑定和自由变量的集合不一定是不相交的,并且可以迭代量词,意味着天真替换产生意外变量捕获,等等.
效率低下的解决方案如下.给定？和？,首先将自由变量分开？和？这样标准化术语中的所有自由变量都大于最大约束变量加上绑定运算符的数量？和？,给？？和？'.然后重命名绑定变量？' 从x 0开始.然后绑定变量？'.然后是？'的自由变量.然后是？'的自由变量.
我想要的是一种更有效的方法来满足问题约束.也就是说,一种不需要重命名自由变量的初始标准化的解决方案.有效地区分变量不是问题.但是,额外的限制给我带来了麻烦.