如何在TLA+中声明非全域且非满射的函数？

TLA+里默认的函数是全域的，但要定义你需要的非全域映射，有两种直接的实现方式：

方式1：用有序对集合表示关系 #

函数本质上是满足“每个定义域元素最多对应一个值域元素”的关系，所以可以直接把SS定义为有序对的集合：

Set1 == {"A","B","C"}
Set2 == {1,2,3}
SS == {<< "A", 1 >>, << "B", 3 >>}

这个集合自动满足函数的约束（每个键只对应一个值），而且只包含你需要的映射，C不在定义域里。

方式2：用部分函数语法[S ->? T] #

TLA+支持显式定义部分函数，语法是[Domain ->? Range]，表示定义域是Domain的子集，每个元素最多映射到Range的一个元素。你可以直接指定SS的定义域和对应的值：

Set1 == {"A","B","C"}
Set2 == {1,2,3}
SS == [s \in {"A", "B"} |-> IF s = "A" THEN 1 ELSE 3]

这里定义域是{"A","B"}（Set1的子集），所以这是个部分函数，C不在定义域内，不会被映射。

区分部分函数和记录 #

你提到容易混淆函数和单键记录，这里明确一下：

• 记录的键必须是标识符（比如a、b这种，不能是字符串字面量"A"），比如[A: 1, B:3]在TLA+里是非法的，因为"A"是字符串不是标识符；
• 函数的定义域可以是任意集合（包括字符串集合、数值集合等），部分函数的定义域是原集合的子集，完全匹配你需要的场景。

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