如何在IDP-Z3中模拟偏函数（partial functions）？

偏函数指仅在定义域的子集上有明确映射的函数，IDP-Z3没有原生支持偏函数，但可以通过以下几种方式模拟：

1. 用关系建模偏函数 #

偏函数本质是“每个定义域元素最多对应一个值域元素”的映射关系，因此可以直接用二元关系表示，再通过断言保证函数的唯一性。

示例代码 #

vocabulary V {
    Domain: type
    Range: type
    PartialFunc: relation(Domain, Range)
}

theory T: V {
    // 核心断言：每个Domain元素最多对应一个Range元素，满足偏函数的唯一性
    forall x: Domain, exists at most one y: Range where PartialFunc(x, y)
}

// 实例化：定义域为整数，仅正整数有映射
structure S: V {
    Domain = {1, 2, 3, -1, -2}
    Range = {2, 4, 5}
    PartialFunc = {(1, 2), (2, 4), (3, 5)}
}

使用方式 #

要判断某个元素x是否在偏函数定义域内，只需检查PartialFunc(x, y)是否存在对应的y；若存在，y即为x的映射值。

2. 带前置条件的函数定义 #

通过给普通函数添加前置条件，限制其有效定义域，同时用特殊值标记未定义的情况。

示例代码 #

vocabulary V {
    Domain: type
    Range: type
    // 定义偏函数的定义域前置条件
    IsInDomain: predicate(Domain)
    f: function(Domain) -> Range
    // 用特殊值表示"未定义"
    Undefined: Range
}

theory T: V {
    // 定义域内的元素执行正常映射
    forall x: Domain, IsInDomain(x) => f(x) = x * 2
    // 非定义域元素映射到Undefined
    forall x: Domain, not IsInDomain(x) => f(x) = Undefined
    // 确保定义域内的结果不会是Undefined
    forall x: Domain, IsInDomain(x) => f(x) != Undefined
}

structure S: V {
    Domain = {1, 2, 3, -1, -2}
    Range = {2, 4, 6, Undefined}
    IsInDomain(x) = x > 0
}

优缺点 #

• 优点：语法更接近普通函数，使用时直接调用f(x)即可，通过判断结果是否为Undefined知晓是否在定义域内。
• 缺点：需要在值域中额外引入Undefined特殊值，可能会增加值域的复杂度。

3. 使用选项类型（Option Type） #

如果IDP-Z3支持代数数据类型（ADT），可以定义选项类型来显式区分“有定义”和“无定义”的情况，这是最直观的现代类型系统风格。

示例代码 #

vocabulary V {
    Domain: type
    Range: type
    // 定义选项类型：要么包含一个Range值（Some），要么表示无定义（None）
    OptionRange: type = Some(Range) | None
    f: function(Domain) -> OptionRange
}

theory T: V {
    // 正整数映射到对应的计算值，其余情况为None
    forall x: Domain, x > 0 => f(x) = Some(x * 2)
    forall x: Domain, x <= 0 => f(x) = None
}

structure S: V {
    Domain = {1, 2, 3, -1, -2}
    Range = {2, 4, 6}
}

使用方式 #

调用f(x)后，若返回Some(y)则表示x在定义域内，映射值为y；若返回None则表示x不在定义域内。

内容的提问来源于stack exchange，提问作者vadevesi