使用占位符快速查找树？
Fast lookup of tree with placeholders?
对于我正在考虑的应用程序，会有大量 (100,000+) 'database' 树（想想编程语言中的表达式或 S 表达式），我需要查询它匹配特定给定表达式的表达式的数据库。
在给出我想要的细节之前，请注意，我很感激 任何 与索引大量树相关的信息以优化子树查找.
在我的特定情况下（Metamath 证明助手使用的后端），表达式具有以下结构（类似于 Haskell 的表示法）：
data Expression = Placeholder Id | VarName Id | ConstName Id [Expression]
或作为 S 表达式形式的 BNF：
Expression = '?' Id | Id | '(' Id Expression* ')'
其中 Id 是某种标识符。
例如，我可以有一个包含像
这样的表达式的数据库
(equiv ?ph ?ps)
(not (in (appl (sqrt) (2)) (Q)))
(equiv (eq ?A ?B) (forall ?x (equiv (in ?x ?A) (in ?x ?B))))
在此上下文中，两个表达式 匹配 如果它们可以通过替换占位符的表达式使它们相等。所以在上面的迷你数据库中查找 (equiv (eq A (emptyset)) ?ph) 会得到第一个和最后一个表达式。
再说一遍：我将如何在大量带有占位符的（表达式）树中实现快速查找？我可以使用什么样的索引数据结构？
我会用 trie 实现查找。每个密钥将包含以下内容之一：
- ConstName 标识符
- 带有上下文信息的变量
- 常量值
- 占位符
这些应该以某种方式排序——可能是占位符，然后是所有 ConstNames（按字母顺序），然后是变量（范围排序，然后是参数顺序），然后是 ConstValues（数字顺序）。只要在 trie 中有具体的使用顺序，就可以了。
遍历表达式的树，在遇到适当的键时将它们注入到 trie 中。对要插入到数据结构中的所有表达式执行此操作。当需要查询时，您可以以类似的方式遍历 trie，但使用一些新规则。
- 一切都匹配一个占位符节点。如果它也匹配其他一些键，那么您将需要探索这两个分支（通过类似递归 DFS 的方法轻松完成）。
- 占位符匹配所有内容。这不等同于前一点 - 我们在这里讨论的是查询中的占位符，上一条将占位符视为 trie 键。
现在，这确实意味着当您遇到占位符时搜索 space 可能会有点 "explode"，但是您可以做一件事来尝试在实践中减轻这种情况。以广度优先的方式遍历表达式的树（在 trie 的构造和查询中）。这意味着如果其中一个参数是占位符，则您不必全面搜索与该表达式匹配的每个子树 到目前为止 - 而是跳到下一个参数-这可能不是占位符，因此会大大减少搜索 space（与匹配 "everything" 相比）。
为了完整起见，让我们举一个例子
(not (in (appl (sqrt) (2)) (Q)))
并从中创建一个 trie 条目-
not -> in -> apply -> "Q" -> sqrt -> 2
向其中添加 (not (in ?ph E)) 将导致-
not -> in -> apply -> "Q" -> sqrt -> 2
\-> ?ph -> "E"
以这种方式继续将表达式注入 trie。也以这种方式遍历以进行查询，直到到达 trie 中的搜索结束，以及 return 匹配的那些。
注意 - 这些条目的唯一性基于您不必支持可变函数的假设。如果这样做，请在每个键上附加一些上下文信息（阅读下一段以了解如何执行此操作的信息）以区分哪些参数转到哪些函数
我忽略了一个细节——变量。如果您只想在它们是完全相同的变量名时匹配，则无需任何工作。但这可能不是您想要的；您可能希望它匹配通用变量，只要它们彼此 "consistent" 即可。这样做的方法是为每个变量分配一个标识符，该标识符代表它最初定义的范围。
最简单的方法就是将其祖先的参数顺序串联起来组成一个标识符。也就是说，如果变量首先被定义为函数的 second 参数，而函数是根函数的 fifth 参数，那么我们可能会标记它作为 (5, 2) 或 (2, 5)，以更直观的为准。无论哪种方式，这都将确保为变量提供一致的标识符，而不管其他地方的其他变量/函数。然后使用这个新变量名称照常进行。
对于我正在考虑的应用程序，会有大量 (100,000+) 'database' 树（想想编程语言中的表达式或 S 表达式），我需要查询它匹配特定给定表达式的表达式的数据库。
在给出我想要的细节之前，请注意，我很感激 任何 与索引大量树相关的信息以优化子树查找.
在我的特定情况下（Metamath 证明助手使用的后端），表达式具有以下结构（类似于 Haskell 的表示法）：
data Expression = Placeholder Id | VarName Id | ConstName Id [Expression]
或作为 S 表达式形式的 BNF：
Expression = '?' Id | Id | '(' Id Expression* ')'
其中 Id 是某种标识符。
例如，我可以有一个包含像
这样的表达式的数据库(equiv ?ph ?ps)
(not (in (appl (sqrt) (2)) (Q)))
(equiv (eq ?A ?B) (forall ?x (equiv (in ?x ?A) (in ?x ?B))))
在此上下文中，两个表达式 匹配 如果它们可以通过替换占位符的表达式使它们相等。所以在上面的迷你数据库中查找 (equiv (eq A (emptyset)) ?ph) 会得到第一个和最后一个表达式。
再说一遍：我将如何在大量带有占位符的（表达式）树中实现快速查找？我可以使用什么样的索引数据结构？
我会用 trie 实现查找。每个密钥将包含以下内容之一：
- ConstName 标识符
- 带有上下文信息的变量
- 常量值
- 占位符
这些应该以某种方式排序——可能是占位符，然后是所有 ConstNames（按字母顺序），然后是变量（范围排序，然后是参数顺序），然后是 ConstValues（数字顺序）。只要在 trie 中有具体的使用顺序，就可以了。
遍历表达式的树，在遇到适当的键时将它们注入到 trie 中。对要插入到数据结构中的所有表达式执行此操作。当需要查询时，您可以以类似的方式遍历 trie，但使用一些新规则。
- 一切都匹配一个占位符节点。如果它也匹配其他一些键，那么您将需要探索这两个分支（通过类似递归 DFS 的方法轻松完成）。
- 占位符匹配所有内容。这不等同于前一点 - 我们在这里讨论的是查询中的占位符，上一条将占位符视为 trie 键。
现在，这确实意味着当您遇到占位符时搜索 space 可能会有点 "explode"，但是您可以做一件事来尝试在实践中减轻这种情况。以广度优先的方式遍历表达式的树（在 trie 的构造和查询中）。这意味着如果其中一个参数是占位符，则您不必全面搜索与该表达式匹配的每个子树 到目前为止 - 而是跳到下一个参数-这可能不是占位符，因此会大大减少搜索 space（与匹配 "everything" 相比）。
为了完整起见，让我们举一个例子
(not (in (appl (sqrt) (2)) (Q)))
并从中创建一个 trie 条目-
not -> in -> apply -> "Q" -> sqrt -> 2
向其中添加 (not (in ?ph E)) 将导致-
not -> in -> apply -> "Q" -> sqrt -> 2
\-> ?ph -> "E"
以这种方式继续将表达式注入 trie。也以这种方式遍历以进行查询，直到到达 trie 中的搜索结束，以及 return 匹配的那些。
注意 - 这些条目的唯一性基于您不必支持可变函数的假设。如果这样做，请在每个键上附加一些上下文信息（阅读下一段以了解如何执行此操作的信息）以区分哪些参数转到哪些函数
我忽略了一个细节——变量。如果您只想在它们是完全相同的变量名时匹配，则无需任何工作。但这可能不是您想要的；您可能希望它匹配通用变量，只要它们彼此 "consistent" 即可。这样做的方法是为每个变量分配一个标识符，该标识符代表它最初定义的范围。
最简单的方法就是将其祖先的参数顺序串联起来组成一个标识符。也就是说，如果变量首先被定义为函数的 second 参数，而函数是根函数的 fifth 参数，那么我们可能会标记它作为 (5, 2) 或 (2, 5)，以更直观的为准。无论哪种方式，这都将确保为变量提供一致的标识符，而不管其他地方的其他变量/函数。然后使用这个新变量名称照常进行。