良类型逻辑程序并非错误

我们考虑逻辑程序的规范类型系统（如Goedel或Mercury所示）。在此类系统中，类型是静态的，但它保证了一个操作属性：如果程序是"良类型"的，那么所有从"良类型"查询开始的派生仍是"良类型"的。这一属性被称为subject reduction。我们表明，这一属性也可以表述为逻辑程序的证词语义属性，从而抽象于通常的运算（自上而下）语义。这一证词语义观点使我们对通常认为必要的条件——即每个子句头部必须具有声明类型的变体（而非真实例）——提出质疑。我们提供了更一般的条件，从而在头部和body原子之间重新建立某种对称性。该条件确保在派生中，两个统一项的类型本身是可统一的。我们讨论了此结果的可能影响。我们还讨论了head条件与多态递归（functional programming中已知的概念）之间的关系。