TML:头元语言 源码

介绍 TML(Tau元语言)是Datalog的变体。它旨在用作形式语言之间的翻译(更多用法,请参见“哲学”部分)。 TML与通用数据记录实现之间的主要区别在于,TML在部分定点(PFP)语义下工作,这与遵循完善语义(WFS)或分层数据记录的通用实现不同。这样,TML(与WFS一样)对否定不施加语法限制,但是与WFS或分层数据日志不同,它是PSPACE完整的,而不是P完整的。 TML的实现很大程度上依赖于内部的BDD(二进制决策图)。这使其在时间和空间方面具有非凡的性能,甚至在大宇宙上也可以进行求反。实际上,归功于BDD机制,如下所述,否定的物体在任何情况下都不会比肯定的物体消耗更多的时间或空间。 尚未实施 尽管实施工作仍在进行中,但并非所有文档都已实施,并且预计将在数周内实施。此外,由于尚未进行测试和最终完成,因此尚未发布。 具体来说: 证明提取需要重写。 包含否定的程序的证明提取。 树提