note-math

对人来说, 一种理解自然数的方式是数数 (counting)

对计算机来说 (cf. #link(<logic.typ>)[]), 表示自然数的方式有

周期电路
算术元件 $+ 1$
二进制

然而, 自然数集的元素数量是无限的, 而 bit 和计算机内存是有限的. 人类的记忆也是有限的

空间无限的问题: 现实无法构建空间无限的电路和内存. 即使能, 也受限于电流速度有限

但是可以使用潜在无限的时间来实现 "潜无限"

然而, 甚至存在集合的元素数量 #link(<uncountable>)[不可数]. Example

the set of all subset of $ℕ$ , $Subset (ℕ)$
all function from $ℕ$ to itself, $ℕ \to ℕ$

验证集合论语言的正确性需要 parser, 内存数据结构, 函数. 生成的计算机指令流的实现并不是这个目标范围的重点

集合/类型的动机

模块化和乘法分解以简化认知

Example 自然语言的主谓宾 SVO (subject, predicate, object). 假设有 10 个名词和 10 个动词. 假设我们 "忘记了 SVO 规则", 那么, 验证三个词的句子的语法正确性最多需要 $10^{3} = 1000$ 次. 如果理解并使用 SVO 规则, 最多需要 $2^{3} = 8$ 次
如果集合的元素数量是无限的, 则集合/类型将概念有限化, 使得可以在有限时间内说出来

复杂的 set theory object (集合论对象), proposition (命题) 被储存在变量名里, 所以还是需要人类去检查所有存储在变量名里面的复杂定义, 所以可读性很重要

parser or 证明辅助程序能让人类从需要检阅所有步骤 reduce to 检阅定义, 跳过大量详细证明步骤, 就能确定证明结果的正确性. 这像 API 的情况

人脑编译器能省略和补充省略, 用容易出错和遗忘来换取临时效率

而且证明辅助还会有其它作用, 类似于, IDE/LSP/友好且互动的编译器错误信息/documentation 时代之前的编程是痛苦的, 数据和信息的组织和结构化和复用做得不好, 也没利用好计算机的强大记忆容量和时间

proposition_(tag) proposition 是特殊的 (string, bool) product struct ((字符串, 真假值) 的逻辑乘积结构) 计算机数据结构. 对于数学语言, string field 使用特殊的构造规则来限制, 此 string 限制版本称为 formula

因为我们无法直接判断一个猜测的真假, 所以我们需要一种具有未定义真假值的语言

from 命题 to 未知命题的, 其真值部分被修改为 (bool, unknow) sum struct

Abbreviation true proposition 和 proposition 经常混用

很多命题是无法被计算机自动推导出来的, 需要人类去寻找可能的路径, 输入到计算机中进行验证, 或者开发更多新的自动化证明方法

我们将假设一些最开始的不需要证明的命题. 以及假设规则之使用现有命题构造新命题

Abbreviation 使用相同的符号 $ϕ$ for formula and proposition, " $ϕ$ is true/false/unknow", $ϕ = 0 / 1 / ?$

formula_(tag)

in (属于)

let symbol (符号) $𝑎, 𝐴$ be type of math object, then $𝑎 \in 𝐴$ is a formula

$𝑎 \in 𝐴$ 类似于 value : type or variable_name : type in programming language

symbol $\in$ 不是 math object

equal (等于)

let

𝑎, 𝑏

be object, then

𝑎 = 𝑏

is a formula

and, or, not (且, 或, 非)

let $𝑝, 𝑞$ be formula, then

\begin{matrix} 𝑝 \land 𝑞 \\ 𝑝 \lor 𝑞 \\ \neg 𝑞 \end{matrix}

is formula

forall, exists (所有, 存在)

设 $𝑝 (𝑎)$ 是用 $𝑎$ 构造的公式 i.e. 在内存中读取 $𝑎 \in 𝐴$ , 使用特殊的函数调用, 则

\begin{matrix} \underset{𝑎 \in 𝐴}{⋀} 𝑝 (𝑎) or \forall 𝑎 \in 𝐴, 𝑝 (𝑎) \\ \underset{𝑎 \in 𝐴}{⋁} 𝑝 (𝑎) or \exists 𝑎 \in 𝐴, 𝑝 (𝑎) \end{matrix}

is formula

inference (推导) $𝑝 \Rightarrow 𝑞$ , equivalent (等价) $𝑝 \Leftrightarrow 𝑞$ is formula

以下讨论 math-object-construct-rule (数学对象构造规则) alias set-theory (集合论)

natural-number_(tag) $ℕ$

natrual number $0, 1, 2, \dots$ and natrual number set $ℕ$ is object. $0, 1, 2, \dots \in ℕ$ is true proposition

但是计算机无法处理无限. 为了让计算机能用有限的字符和内存去表示自然数集, 把 $𝑛, ℕ$ 和 $+ 1$ 函数作为内存地址里的有限 symbol, 定义以下为 true proposition

$0 \in ℕ$
$𝑛 \in ℕ ⟹ 𝑛 + 1 \in ℕ$

等价于用指令流告诉计算机如何连续地 $+ 1$ ? 也联系到归纳法

有限的字符的代价是潜在无限的时间, 总是借助了数数或者周期电路

empty_(tag) $\emptyset$

empty $\emptyset$ is object. let $𝑎$ be a object, $𝑎 \in \emptyset$ is false proposition

The definition of $\emptyset$ 方便用于 intersections $\cap$ e.g. 交集为空, 和有限集 $𝐴$ 的 $Subset (𝐴)$ 的元素数量, $2^{𝑛}$ 比 $2^{𝑛} - 1$ 方便

定义语言展开

$𝑎 \neq 𝑏 ≔ \neg (𝑎 = 𝑏)$
$𝑎 \notin 𝐴 ≔ \neg (𝑎 \in 𝐴)$

由于 “定义语言展开” 很长, 因此通常 abbreviated to "definition" "def"

其实 symbol $=$ 通常也被用来表示定义语言展开或者规定语言转化. 具体自然数的 $=$ 可以直接定义为用计算机电路比较内存的值

declare-element-of-set_(tag)

If $𝐴$ is non empty $𝐴 \neq \emptyset$ (此信息来自 $𝐴$ 的定义), we can define symbol $𝑎$ and construct true proposition (let) $𝑎 \in 𝐴$

可以构造有限个 declare 语句

enum_(tag) enumerate

$𝑎_{0}, \dots, 𝑎_{𝑛}$ is object then ${𝑎_{0}, \dots, 𝑎_{𝑛}}$ is a set

表示为内存里的数列

整个集合可以被这样调用: 记录第一个元素地址 + 数组长度作为电路周期数量, 每个电路周期读取一个元素

formulas $𝑎_{0}, \dots, 𝑎_{𝑛} \in {𝑎_{0}, \dots, 𝑎_{𝑛}}$ are true propositions

特别地, 单元素集合 $𝑎 \in {𝑎}$

define $𝐴 \subset 𝐵 ≔ \forall 𝑎 \in 𝐴, 𝑎 \in 𝐵$

equivalent_(tag) $⟺$

等价的一些使用. 对计算机数据来说, 可以穷举证明以下计算结果相等

\begin{matrix} \neg (\neg 𝑝) & ⟺ & 𝑝 \\ \neg (𝑝 \land 𝑞) & ⟺ & (\neg 𝑝) \lor (\neg 𝑞) \end{matrix}

类似地, 为了表示 "无限元素" 的情况, 定义语言展开或者规定语言转化. 例如无限元素的 De Morgan law

\begin{matrix} \neg (\underset{𝑎 \in 𝐴}{⋀} 𝑝 (𝑎)) & ⟺ & \underset{𝑎 \in 𝐴}{⋁} \neg 𝑝 (𝑎) \\ or \neg (\forall 𝑎 \in 𝐴, 𝑝 (𝑎)) & ⟺ & \exists 𝑎 \in 𝐴, \neg 𝑝 (𝑎) \end{matrix}

其中 "无限" 的概念有的限化是使用 #link(<declare-element-of-set>)[] 的符号串 $𝑎 \in 𝐴$

formula, proposition 是内存里特殊的数据结构. 可以认为 math_object, formula, proposition 是编程语言的 type

许多命题是等价的, 于是可以考虑命题的 "quotient" 类型, 但等价可能性是无限的, 是否可能从存在穷举算法, 首先要看它是否 #link(<countable>)[] …

类似 $\land, \lor, \neg$ 的冗余, set theory construction rules 也有可能有冗余, 或者说有很多等价的定义方式

规定 (有限的)

$=$ transitive := $(𝑎 = 𝑏) \land (𝑏 = 𝑐) ⟹ (𝑎 = 𝑐)$

$\Leftrightarrow$ transitive := $(𝑝 \Leftrightarrow 𝑞) \land (𝑞 \Leftrightarrow 𝑟) ⟹ (𝑝 \Leftrightarrow 𝑟)$

follow #link(<bool-algebra>)[有限情况的 bool 的各种规则], 定义语言转换规则: let $𝑝 (𝑎, 𝑏)$ is formula built with independent/parallel $𝑎, 𝑏$ i.e. independent/parallel in memory read and used by specific cuntion, then

commutative-forall-exists_(tag)

\underset{𝑎 \in 𝐴}{⋀} \underset{𝑏 \in 𝐵}{⋀} 𝑝 (𝑎, 𝑏) ⟺ \underset{𝑏 \in 𝐵}{⋀} \underset{𝑎 \in 𝐴}{⋀} 𝑝 (𝑎, 𝑏)

same for $⋁$

distributive-forall-exists_(tag)

\underset{𝑎 \in 𝐴}{⋀} \underset{𝑏 \in 𝐵}{⋁} 𝑝 (𝑎, 𝑏) ⟺ \underset{𝑏 \in 𝐵}{⋁} \underset{𝑎 \in 𝐴}{⋀} 𝑝 (𝑎, 𝑏)

注意, 我自己也觉得我无法完全清晰地处理下面的推导和证明的概念

推导的自然语言例子

如果下雨, 我不会出门
下雨了
所以我不会出门

这个例子类似于 conditional branch (条件分支)

rain : bool;
out : bool;
switch (rain) {
  true => out = false,
  false => out = undefined
};

inference_(tag) 对于数学语言, 那就是

编译器读取到 formula $𝑝, 𝑞$
编译器读取到 formula $𝑝 \Rightarrow 𝑞$ is true proposition (可能来自定义)
编译器读取到 formula $𝑝$ is true proposition
然后语言规则设置是, 编译器根据这种条件 (来自内存), 赋予 formula $𝑞$ 的 bool 值为 true i.e. 设置 $𝑞$ is true proposition

proof_(tag) 证明就是编译通过 $𝑝 \Rightarrow 𝑞$ is true proposition

又一种等价 $𝑝 \Leftrightarrow 𝑞 ≔ (𝑝 \Rightarrow 𝑞) \land (𝑞 \Rightarrow 𝑝)$

reverse-inference_(tag) 反向推导. 如果结果是我出门了, 那么肯定不是下雨的结果. 如果条件分支的结果是 out = true, 这不是 rain = true 的结果. 由于理想二进制计算机的 bool 值必定二选一, 所以只能是 rain = false 的结果. 这可以被写为条件分支

switch (out) {
  true => rain = false,
  false => rain = undefined
};

数学上, 反向推导写为 formula $\neg 𝑞 \Rightarrow \neg 𝑝$ , 并定义等价到 $𝑝 \Rightarrow 𝑞$

reverse-proof_(tag) 反证明就是编译通过 $\neg 𝑝 \Rightarrow \neg 𝑞$ is true proposition

演绎证明还需要三段论 (syllogism)

所有生物都会死
人是生物
所以所有人都会死

其中 "所有生物都会死" 是特殊构造的一种命题

syllogism_(tag) 三段论推导是语言规则

编译器读取到 formula $(\forall 𝑎 \in 𝐴, 𝑝 (𝑎))$ is true proposition (可能来自定义 e.g. #link(<union>)[]))
编译器读取到声明 let $𝑎^{'} \in 𝐴$ is true proposition
编译器读取到 formula $𝑝 (𝑎^{'})$
然后编译器根据这种条件 (来自内存) 设置 $𝑝 (𝑎^{'})$ is true proposition

也即, 编译器根据声明 $(\forall 𝑎 \in 𝐴, 𝑝 (𝑎))$ (可能 "无限") 来实现对数据的具体构造 (有限)

或者理解为, 这种规则和行为就是在定义 $(\forall 𝑎 \in 𝐴, 𝑝 (𝑎))$ 这种概念本身

通常也被写为等价的规则 let $𝑎^{'} \in 𝐴$ , then 特殊的推导 formula $(\forall 𝑎 \in 𝐴, 𝑝 (𝑎)) ⟹ 𝑝 (𝑎^{'})$ is always true proposition. 这种形式通常被用于 #link(<proof>)[前面] 所说的 "证明就是编译通过 $𝑝 \Rightarrow 𝑞$ is true proposition"

反向三段论: let $𝑎^{'} \in 𝐴$ , then 等价的 formula $\neg 𝑝 (𝑎^{'}) ⟹ \neg (\forall 𝑎 \in 𝐴, 𝑝 (𝑎)) or \exists 𝑎 \in 𝐴, \neg 𝑝 (𝑎)$ is true proposition

我们可能永远不知道一个 bool unknow 的 proposition 是否能被构造性地证明, i.e. 有限步骤编译成功

target proposition 来自哪里? 可能是相关于现实世界的模型

证明需要展开大量句子, 尽管计算机处理 string 是非常快的. 无论如何, 性能优化? 仅在需要时使用 (lazy load)? 两个 proposition 不相互依赖时, 并行 (parallel)? 假设已经证明过的结果 (incremental compilation)?

A proposition has many proofs with different runtime data flow, 可以认为它们属于同一个 quotient proof of this proposition

以下的 object construction rules, 除了交集, 一般都给出 non-emtpy sets

union_(tag)

define object $⋃ 𝐴$ 和语言展开

\begin{matrix} 𝑥 \in 𝑎 \cup 𝑎^{'} & ≔ & (𝑥 \in 𝑎) \lor (𝑥 \in 𝑎^{'}) \\ 𝑥 \in ⋃ 𝐴 & ≔ & \underset{𝑎 \in 𝐴}{⋁} 𝑥 \in 𝑎 \\ ≔ & \exists 𝑎 \in 𝐴, 𝑥 \in 𝑎 \end{matrix}

is non-emtpy unless $\forall 𝑎 \in 𝐴, 𝑎 = \emptyset$

$𝐴 \cup 𝐴 = 𝐴$

我们不对 $𝐴 = \emptyset$ 定义 union. 下同. 理由是 let $𝑎 \in 𝐴 = \emptyset$ is always false proposition, 这使得很多东西不能用

sum_(tag)

\begin{matrix} 𝑥 \in 𝑎 ⊔ 𝑎^{'} & ≔ & (𝑥 \in 𝑎) \oplus (𝑥 \in 𝑎^{'}) \\ 𝑥 \in ⨆ 𝐴 & ≔ & ⨁_{𝑎 \in 𝐴} 𝑥 \in 𝑎 \\ ≔ & \exists! 𝑎 \in 𝐴, 𝑥 \in 𝑎 \end{matrix}

is non-emtpy unless $\forall 𝑎 \in 𝐴, 𝑎 = \emptyset$

in finite case, number of element $| ⨁_{1}^{𝑛} 𝐴_{𝑖} | = \sum_{1}^{𝑛} | 𝐴_{𝑖} |$

enum is special case of sum/union?

intersection_(tag)

\begin{matrix} 𝑥 \in 𝑎 \cap 𝑎^{'} & ≔ & (𝑥 \in 𝑎) \land (𝑥 \in 𝑎^{'}) \\ 𝑥 \in ⋂ 𝐴 & ≔ & \underset{𝑎 \in 𝐴}{⋀} 𝑥 \in 𝑎 \\ ≔ & \forall 𝑎 \in 𝐴, 𝑥 \in 𝑎 \end{matrix}

$𝐴 \cap 𝐴 = 𝐴$

product_(tag)

\begin{matrix} 𝑥 \in 𝑎 \times 𝑎^{'} & ≔ & (𝑥 (𝑎) \in 𝑎) \land (𝑥 (𝑎^{'}) \in 𝑎^{'}) \\ 𝑥 \in \prod 𝐴 & ≔ & \underset{𝑎 \in 𝐴}{⋀} 𝑥 (𝑎) \in 𝑎 \\ ≔ & \forall 𝑎 \in 𝐴, 𝑥 (𝑎) \in 𝑎 \end{matrix}

is non-emtpy unless $\exists 𝑎 \in 𝐴, 𝑎 = \emptyset$ (related to axiom-of-choice_(tag) )

Abbreviation $𝐴 \times 𝐴 = 𝐴^{2}$ . in finite case, number of elements $| \prod_{1}^{𝑛} 𝐴_{𝑖} | = \prod_{1}^{𝑛} | 𝐴_{𝑖} |$

$𝑥 (𝑎)$ 表示将两个 symbol 作为一个组合 symbol 来读取

map_(tag)

let $𝐴, 𝐵$ is math object. 定义 map space $𝐴 \to 𝐵$ , map $𝑓$ as math object 的规则是

\begin{matrix} 𝑓 \in (𝐴 \to 𝐵) & ≔ & \underset{𝑎 \in 𝐴}{⋀} 𝑓 (𝑎) \in 𝐵 \\ ≔ & \forall 𝑎 \in 𝐴, 𝑓 (𝑎) \in 𝐵 \end{matrix}

denoted by $𝑓 : 𝐴 \to 𝐵$

denoted by $𝑓 \in 𝐵^{𝐴}$ . in finite case, number of elements $| 𝐵^{𝐴} | = | 𝐵 |^{| 𝐴 |}$

$𝑓, 𝑓 (𝑎), 𝑓 (𝑎) \in 𝐵$ 的使用虽然看起来有问题, 但它们仍然在 symbol & symbol 串方面是可以定义的

如果谈到 map $𝑓$ 具体代表什么, 由于非具体构造性, 没有一般编程语言那样的具体的 return, 或者 return 的是新定义的 symbol, math object, 语言展开

subset_(tag)

𝑆 \in Subset (𝐴) ≔ 𝑆 \subset 𝐴

denoted by $2^{𝐴}$ . 根据 #link(<proposition-function>)[] 等价于 map space $𝐴 \to {0, 1}$ . in finite case, number of elements $| 2^{𝐴} | = 2^{| 𝐴 |}$

define $\emptyset \subset 𝐴$ be true proposition

map space 和 subset 引入了高级别的无限

一件初看反直觉的事情是, 我们似乎知道所有 $𝑆 \subset ℕ$ 或所有 $𝑓 : ℕ \to ℕ$ , 却无法数出来 #link(<cardinal-increase>)[] #link(<uncountable>)[]. 但是, "知道所有 $𝑆 \subset ℕ$ " 究竟是什么意思? 事实上, 试着考虑 "一般方式之找一个 $ℕ$ 的无限子集" 这一个问题, 就会发现这不是简单的

类似地, 虽然可数已经可以定义一些实数 e.g. $\sum \frac{1}{𝑛!} = 𝑒$ , 但如果不借助 subset or map, 可数地构造无法得到全部 $ℝ$

proposition-function_(tag)

let $𝑎 \in 𝐴$ , $𝑝 (𝑎) : 𝐴 \to {0, 1}$ is already constructed

${𝑎 \in 𝐴 : 𝑝 (𝑎)}$ is object

𝑥 \in {𝑎 \in 𝐴 : 𝑝 (𝑎)} ≔ (𝑥 \in 𝐴) \land 𝑝 (𝑥)

define

𝐴 = 𝐵 ≔ (𝑥 \in 𝐴) ⟺ (𝑥 \in 𝐵)

$=$ 的其它用法

内存里的 identifier 的别名
内存里的函数返回值. so $1 + 1 = 2$ 应该理解为 add function 的返回值是 $2$

hierarchy-order-of-set_(tag)

以上构造的 set 称为 zero (hierarchy) order set

$𝐴 \in Set$ or $𝐴 \in Set 0$

then let $Set 0$ be math object, in first order set

$Set 0 \in Set 1$

再次使用 object construction rules, 得到的东西也定义为属于 $Set 1$

无论如何我们总是可以在编译器中构造这种带有类型和 bool 和各种规则的语言. 虽然还有编译器的编译器, 编译器的层数也可以是无限的 …

let $Set 1$ be math object, $Set 1 \in Set 2$ . 诸如此类 …

Example

$Set \times Set \in Set 1$
$(Set \to Set) \in Set 1$
$Group \in Set 1$
$\begin{matrix} (𝐺, 𝑚) \in Group ≔ \\ 𝐺 \in Set \\ 𝑚 \in Set \\ property-group-multiplication (𝐺, 𝑚) \\ (e.g. 𝑚 \in (𝐺^{2} \to 𝐺)) \end{matrix}$
可以被分成多句, 使得可以方便的加入/移除 property, 来得到不同的 struct

$Set 0, Set 1, \dots$ 看起来像自然数集 $ℕ$ , 所以应该再假设新的 hierarchy $Set ℕ$ 吗? 然后对 $Set ℕ$ , 继续使用 object construct rule …

上面的构造规则会导致矛盾或者计算机死循环吗?

一直无限地构造下去, 这种语言是否有终点?

universal-set_(tag)

是否存在 "set of every set", a "universal set"? or "universal type"?

使用 set theory rules 定义

𝐴 ≔ {𝑥 \in universal-set : \neg (𝑥 \in 𝑥)} \in universal-set

然后让编译器去计算命题 $𝐴 \in 𝐴$ 的 bool, 由于 $𝐴 \in universal-set$ = true, 编译器只计算 $\neg (𝐴 \in 𝐴)$ 的 bool, 然后发现 not 函数, 所以计算 not 里面的 bool, 但这又回到了计算 $𝐴 \in 𝐴$ 的 bool, 编译器可能选择进入电路死循环

对于有限集, $𝑥 \notin 𝑥$ 或者无法判断, e.g. ${1} \notin {1}$ , 因为 $1 \neq {1}$ , 或者没有定义 $𝑥 \in 1$ is true proposition

相关于自指悖论. Example "这个句子是错的" 给出计算机死循环

this_sentence_is_false : bool = false;
loop:
  switch (this_sentence_is_false) {
    false => this_sentence_is_false = true,
    true => this_sentence_is_false = false
  } 
  goto loop
};

或者用分层绕过自指悖论 (this_sentence = false) = true. 认为它们是不同的句子和判断, 认为它并不能自指

如果对于一个数我们能数出来, 我们就认为它是自然数

如果能用有限步写出语言规则并构造出语言对象, 我们就认为是可构造的, 可说的. 对于集合论, 能够这样有限步构造出来的, 就称其为 math object (数学对象)

对于自然数的无限的问题, 如果用数数或者归纳法或者周期电路来定义自然数, 的则把无限的问题推给了无限时间

对于集合论语言, 假设 universal-set or universal-type 导致能构造出让电路进入死循环

dependent-distributive_(tag)

union & interset

⋂_{𝑎 \in 𝐴} ⋃_{𝑥 \in \prod 𝐴} 𝑥 (𝑎) = ⋃_{𝑥 \in \prod 𝐴} ⋂_{𝑎 \in 𝐴} 𝑥 (𝑎)

⋃_{𝑎 \in 𝐴} ⋂_{𝑥 \in \prod 𝐴} 𝑥 (𝑎) = ⋂_{𝑥 \in \prod 𝐴} ⋃_{𝑎 \in 𝐴} 𝑥 (𝑎)

sum and product

\prod_{𝑎 \in 𝐴} ⨆_{𝑥 \in \prod 𝐴} 𝑥 (𝑎) = ⨆_{𝑥 \in \prod 𝐴} \prod_{𝑎 \in 𝐴} 𝑥 (𝑎)

⨆_{𝑎 \in 𝐴} \prod_{𝑥 \in \prod 𝐴} 𝑥 (𝑎) = \prod_{𝑥 \in \prod 𝐴} ⨆_{𝑎 \in 𝐴} 𝑥 (𝑎)

draft of proof: 展开, 使用 parallel distributive cf. #link(<distributive-forall-exists>)[]

set-minus_(tag)

$𝐴 ∖ 𝐵 ≔ {𝑥 \in 𝐴 : 𝑥 \notin 𝐵}$ . if $𝐵 \subset 𝐴$ then define $𝐵^{∁} ≔ 𝐴 ∖ 𝐵$

symmetric-set-minus_(tag)

$𝐴 Δ 𝐵 ≔ (𝐴 ∖ 𝐵) ⊔ (𝐵 ∖ 𝐴) = (𝐴 \cup 𝐵) ∖ (𝐴 \cap 𝐵)$

coordinate-component_(tag)

product component
$\begin{matrix} \prod 𝐴 & ⟶ & 𝑎 \\ 𝑥 & ⟿ & 𝑥 (𝑎) \end{matrix}$
sum component
$\begin{matrix} 𝑎 & ⟶ & ⨆ 𝐴 \\ 𝑥 & ⟿ & 𝑥 (𝑎) \end{matrix}$