小编amk*_*a00的帖子

假设我正在定义一个返回types.SimpleNamespace 的函数。我想输入提示结果：

from types import SimpleNamespace

def func() -> SimpleNamespace(x: int, y: str):  # SyntaxError! What should be used instead?
    return SimpleNamespace(x=3, y='abc')

请注意，通常用作数据成员命名SimpleNamespace的替代方法。tuple对于元组，存在相应的类型提示：

from typing import Tuple

def func() -> Tuple[int, str]:  # OK
    return 3, 'abc'

顺便说一句，今天我使用以下内容作为文档：

from types import SimpleNamespace

def func() -> SimpleNamespace(x=int, y=str):  # Seems to work fine
    return SimpleNamespace(x=3, y='abc')

但这不是标准的（因此类型检查器不支持它），并且可能不是正确的Python（或者是吗？）。

我想在一些可能被称为完全声明的Horn逻辑(或完全声明的Prolog)中形式化一些知识并执行查询.任何人都可以提供一些如何实施它的指导方针吗？我简要回顾一下上面链接中的精细描述:

形式语言是Prolog的核心语言:"程序"是Prolog中的一组规则和事实(包括函数和变量,基本上只包含用户定义的谓词).

然而,与Prolog相比,我正在寻找一种完整的逻辑程序标准声明语义 - 最少Herbrand模型(即归纳定义的基础术语集).在逻辑编程的理论工作中,这通常是研究的对象,众所周知,可以获得对查询的完整和完整的答案(在"递归可枚举的"意义上),例如,使用SLD解析以下条件:

• 公平搜索匹配规则(例如,Prolog的深度优先搜索不公平);
• 与" 发生检查 " 统一(检查变量在与其统一的术语中不会发生).

我正在寻找一个简洁的实现,它将建立在现有功能的基础上,而不是发明轮子.我看到的两个更有希望的方向是将它作为Prolog的元解释器实现,或者作为一些定理证明器的一部分.任何在这些领域具有实践知识的人都能提供一些如何实施它的指导方针吗？可以在miniKanren中轻松实现吗？

我的意图是以完全陈述的方式形式化一些知识.这种形式化的关键特征是它精确地对应于(单调)归纳的数学概念,因此可以通过归纳论证容易地推理知识及其属性.