公理与理论库
Foundations & Theory &
- 公理原则
- 定义模型
- 定理结果
- 应用方法
Mathematics
数学
从逻辑与结构出发,建立离散、连续与空间的共同语言。
Theoretical Computer Science
理论计算机科学
研究什么能够被计算、需要多少资源,以及程序为何正确。
数学
381 条匹配逻辑与基础
命题、证明、公理系统与集合论基础。
- 公理集合外延性公理Axiom of extensionality两个集合恰在拥有相同元素时相等。1 个前置
- 公理选择公理Axiom of choice任意非空集合族都存在一个同时从每个成员中选取元素的选择函数。2 个前置2 个后续
- 原则超限归纳法Transfinite induction若性质在每个序数处由所有更小序数上的成立推出,则它对全部序数成立。1 个前置
- 原则存在唯一性证明Existence and uniqueness proof分别证明至少存在一个对象以及任意两个候选对象相等。1 个前置
- 原则反证法Proof by contradiction假设目标命题为假并推出矛盾,从而证明目标。1 个前置
- 原则分类讨论证明Proof by cases把所有可能情形穷尽划分并在每个情形中证明结论。1 个前置
- 原则康托对角线论证Cantor diagonal argument通过在第 n 位偏离第 n 个候选对象构造未被枚举对象的方法。2 个前置
- 原则肯定前件Modus ponens从命题 P 和蕴含 P→Q 推出 Q 的基本推理规则。1 个前置
- 原则连续统假设Continuum hypothesis断言自然数幂集的基数等于第一个不可数基数的独立集合论命题。2 个前置
- 原则逆否证明法Proof by contrapositive通过证明 ¬Q→¬P 来证明 P→Q。1 个前置
- 原则强归纳法Strong induction归纳步可假设所有较小自然数情形成立。1 个前置
- 原则数学归纳法Mathematical induction由基例和从 n 到 n+1 的归纳步推出性质对全部自然数成立。1 个前置6 个后续
- 原则直接证明Direct proof从假设和已知事实经有效推理直接导出结论。1 个前置
- 定义阿列夫层级Aleph hierarchy按序数索引全部无限初始序数从而枚举无限基数的层级。3 个前置1 个后续
- 定义变量赋值Variable assignment把自由变量映射到结构论域元素的函数。2 个前置1 个后续
- 定义不可数集Uncountable set不存在自然数枚举的集合。1 个前置
- 定义超滤子Ultrafilter集合的幂集上满足向上封闭、有限交封闭并对每个子集作二择一判定的极大滤子。2 个前置1 个后续
- 定义初等嵌入Elementary embedding保持所有一阶公式真值的结构间单射。3 个前置
- 定义单射Injective function不同输入必有不同输出的函数。1 个前置4 个后续
- 定义等价关系Equivalence relation满足自反、对称和传递性的关系。1 个前置9 个后续
- 定义笛卡尔积Cartesian productA×B 是所有第一分量来自 A、第二分量来自 B 的有序对组成的集合。2 个前置9 个后续
- 定义关系Relation从 A 到 B 的二元关系是 A×B 的子集。2 个前置12 个后续
- 定义函数Function每个定义域元素恰对应一个陪域元素的关系。1 个前置74 个后续
- 定义函数复合Function composition按先 f 后 g 的次序把映射串联为 g∘f。1 个前置4 个后续
- 定义合取范式Conjunctive normal form由若干析取子句之合取构成且与原公式逻辑等价的标准形。2 个前置
- 定义基数Cardinality以集合间是否存在双射来比较集合大小。1 个前置15 个后续
- 定义基数算术Cardinal arithmetic以不交并、笛卡尔积和函数集刻画集合基数的加法、乘法与幂。2 个前置
- 定义集合Set由确定成员组成的数学对象;成员关系而非表示顺序决定集合。22 个后续
- 定义集合运算Set operations并、交、差与补集等按成员条件构造新集合的运算。1 个前置14 个后续
- 定义可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。1 个前置1 个后续
- 定义可数集Countable set有限或可与自然数集合建立双射的集合。2 个前置5 个后续
- 定义逻辑等价Logical equivalence两个公式在每个赋值下具有相同真值。1 个前置2 个后续
- 定义满射Surjective function陪域中每个元素都有至少一个原像的函数。1 个前置3 个后续
- 定义满足关系Satisfaction relation用对公式构造的递归定义刻画结构与赋值何时满足一阶公式。3 个前置4 个后续
- 定义幂集Power set集合 A 的所有子集组成的集合,记作 P(A)。2 个前置9 个后续
- 定义逆函数Inverse function与双射复合后得到相应恒等映射的反向函数。2 个前置2 个后续
- 定义偏序Partial order满足自反、反对称和传递性的关系。1 个前置9 个后续
- 定义全序Total order任意两个元素都可比较的偏序。1 个前置18 个后续
- 定义商集Quotient set等价关系的所有等价类组成的集合。2 个前置5 个后续
- 定义双射Bijective function同时为单射和满射的函数。2 个前置4 个后续
- 定义析取范式Disjunctive normal form由若干合取项之析取构成且与原公式逻辑等价的标准形。2 个前置
- 定义形式系统Formal system由符号、形成规则、公理与推导规则组成的精确定义系统。9 个后续
- 定义序数Ordinal由属于关系良序且具有传递性的集合,表征良序的同构类型。2 个前置4 个后续
- 定义序数算术Ordinal arithmetic通过超限递归定义的序数加法、乘法与幂运算,通常不满足交换律。2 个前置
- 定义一阶理论First-order theory同一一阶语言中一组句子及其模型类所构成的理论。2 个前置2 个后续
- 定义一阶逻辑语法First-order syntax以符号表、项、原子公式、联结词和量词归纳生成一阶公式的语法系统。2 个前置3 个后续
- 定义永真式Tautology在每个真值赋值下均为真的命题公式。1 个前置
- 定义有序对Ordered pair区分第一、第二分量且由分量逐项相等刻画相等性的二元对象。1 个前置3 个后续
- 定义语义蕴涵Semantic entailment所有满足前提集的赋值也满足结论时成立的语义关系。2 个前置1 个后续
- 定义子集Subset集合 A 的每个元素都属于 B 时,称 A 是 B 的子集。1 个前置19 个后续
- 定义自由变量与约束变量Free and bound variables按量词作用域区分公式中由赋值决定的变量出现和被量化绑定的变量出现。1 个前置1 个后续
- 模型超积Ultraproduct按超滤子诱导的等价关系对一族结构的直积取商所得的结构。3 个前置1 个后续
- 模型命题逻辑Propositional logic研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。1 个前置17 个后续
- 模型皮亚诺算术Peano arithmetic用一阶语言公理化自然数的零、后继、加法、乘法与归纳模式的形式理论。2 个前置1 个后续
- 模型相继式演算Sequent calculus以左右公式序列构成相继式并用结构规则和逻辑规则推导的证明演算。2 个前置1 个后续
- 模型一阶结构First-order structure为一阶语言中的常元、函数符号和关系符号指定集合上解释的数学结构。4 个前置4 个后续
- 模型一阶逻辑First-order logic在命题逻辑上加入对象、关系、函数与量词的形式语言和模型语义。1 个前置8 个后续
- 模型真值表Truth table按命题变元的全部赋值逐行计算复合公式真值的有限表格模型。1 个前置1 个后续
- 模型自然数模型Natural numbers由零元、后继和二阶归纳原则范畴性刻画的离散数系模型。2 个前置28 个后续
- 模型自然演绎Natural deduction用引入规则与消去规则直接刻画逻辑联结词推理行为的证明演算。2 个前置
- 模型ZF 集合论ZF set theory用一阶语言中的成员关系和一组公理作为现代数学的集合论基础。1 个前置1 个后续
- 定理超限递归定理Transfinite recursion theorem允许用所有较早阶段的值唯一地定义序数长度函数的递归定理。2 个前置1 个后续
- 定理哥德尔第一不完备定理Gödel's first incompleteness theorem足够强、有效公理化且一致的算术理论存在既不可证也不可否证的句子。2 个前置1 个后续
- 定理康托–施罗德–伯恩斯坦定理Cantor–Schröder–Bernstein theorem若 A 可单射到 B 且 B 可单射到 A,则 A 与 B 之间存在双射。2 个前置
- 定理良序定理Well-ordering theorem每个集合都能赋予一个使任意非空子集具有最小元的全序。2 个前置1 个后续
- 定理命题紧致性定理Propositional compactness theorem一个命题公式集可满足,当且仅当它的每个有限子集可满足。2 个前置
- 定理命题逻辑可靠性与完备性定理Soundness and completeness of propositional logic命题演算中的可证性与对所有赋值成立的语义蕴涵恰好一致。2 个前置
- 定理切消定理Cut-elimination theorem相继式演算中的切规则可被消去,从而得到只使用子公式的证明。1 个前置
- 定理一阶逻辑可靠性定理Soundness theorem for first-order logic一阶证明系统中可证的公式在每个模型中都语义有效。2 个前置
- 定理一阶逻辑完备性定理Gödel completeness theorem每个语义有效的一阶公式都可在合适证明系统中形式证明。2 个前置
- 定理一阶替换引理Substitution lemma for first-order logic语法上的无捕获项替换与语义上的变量赋值更新相一致。2 个前置
- 定理佐恩引理Zorn's lemma若偏序集中每条链都有上界,则该偏序集存在极大元。2 个前置1 个后续
- 定理Gödel 第二不完备定理Gödel's second incompleteness theorem足够强且一致的可有效公理化理论不能在自身内部证明自身的一致性。2 个前置
- 定理Łoś 定理Łoś theorem超积中一阶公式成立,当且仅当其分量成立的指标集合属于所用超滤子。2 个前置
- 定理Löwenheim–Skolem 定理Löwenheim–Skolem theorem有无限模型的一阶理论在适当基数上存在较小或较大的模型。2 个前置
代数与结构
运算、群、映射以及结构保持关系。
- 原则泛性质Universal property通过与所有候选对象之间唯一因子化性质刻画对象的同构类。2 个前置1 个后续
- 定义阿贝尔群Abelian group群运算满足交换律的群。1 个前置3 个后续
- 定义半群Semigroup带有结合二元运算的集合。1 个前置1 个后续
- 定义半直积Semidirect product由一个群对另一群的作用扭曲直积运算得到的群构造。3 个前置
- 定义伴随Adjunction两个反向函子之间由自然同构的态射集双射刻画的关系。2 个前置
- 定义不可约元Irreducible element非零非单位且不能分解为两个非单位乘积的整环元素。1 个前置2 个后续
- 定义代数元Algebraic element作为基域上某个非零多项式根的扩域元素。2 个前置1 个后续
- 定义单群Simple group除平凡子群和自身外没有正规子群的非平凡群。2 个前置
- 定义单位与零因子Unit环中的可逆元素,以及能与某个非零元素相乘得到零的非零元素。1 个前置
- 定义对角化Diagonalization在线性算子存在由特征向量构成的基时把其矩阵化为对角形。2 个前置1 个后续
- 定义对偶空间Dual space给定向量空间到标量域的全部线性泛函组成的向量空间。2 个前置
- 定义多项式环Polynomial ring系数来自给定环、以形式不定元构造的多项式集合。2 个前置4 个后续
- 定义二次剩余Quadratic residue模奇素数同余于某个平方的非零剩余类。2 个前置1 个后续
- 定义二元运算Binary operation把集合中任意一对有序元素映回该集合的函数。2 个前置4 个后续
- 定义范畴Category由对象、态射、结合的复合与单位态射构成的抽象结构。2 个前置3 个后续
- 定义分裂域Splitting field使给定多项式完全分裂且由其全部根生成的最小扩域。2 个前置1 个后续
- 定义函子Functor保持单位态射和复合的范畴之间映射。2 个前置3 个后续
- 定义环Ring带加法阿贝尔群和相容乘法的代数结构。2 个前置9 个后续
- 定义环的局部化Localization of rings把指定乘法闭集中的元素形式地变为可逆元所得的环。3 个前置
- 定义环同态Ring homomorphism保持加法与乘法的映射;含幺语境中是否要求保持 1 必须明确。2 个前置
- 定义基Basis of a vector space同时线性无关并张成整个向量空间的向量组。2 个前置4 个后续
- 定义极大理想Maximal ideal在真理想按包含关系中极大的理想,其商环为域。3 个前置
- 定义极小多项式Minimal polynomial以给定代数元为根的首一不可约多项式。2 个前置
- 定义迹Trace of a matrix方阵主对角元素之和,也是线性算子在换基下不变的标量。1 个前置
- 定义伽罗瓦群Galois group固定基域的扩域自同构在复合下形成的群。2 个前置1 个后续
- 定义交换环Commutative ring乘法满足交换律的环。1 个前置7 个后续
- 定义交换子群Commutator subgroup由全部交换子生成的正规子群,度量群偏离交换性的程度。2 个前置1 个后续
- 定义矩阵Matrix按行列排列域元素并支持线性组合与乘法的有限二维数组。2 个前置8 个后续
- 定义可解群Solvable group导出列在有限步后降为平凡群的群。2 个前置
- 定义理想Ideal对加法成子群且吸收环乘法的子集。2 个前置6 个后续
- 定义模Module以环元素作标量、以阿贝尔群作加法结构并满足分配律的代数结构。2 个前置4 个后续
- 定义模同态Module homomorphism同时保持加法与标量乘法的模之间映射。2 个前置1 个后续
- 定义模同余Congruence modulo n两整数之差被给定正整数整除时成立的等价关系。2 个前置4 个后续
- 定义内积空间Inner product space带正定对称双线性形式或复数情形共轭对称形式的向量空间。2 个前置5 个后续
- 定义欧几里得整环Euclidean domain带有允许带余除法并严格下降的欧几里得函数的整环。2 个前置
- 定义欧拉函数Euler totient function计数不超过 n 且与 n 互素的正整数的算术函数。2 个前置
- 定义陪集Coset固定群元素与子群相乘得到的左陪集或右陪集。2 个前置
- 定义群Group具有结合运算、单位元和每个元素逆元的集合。1 个前置19 个后续
- 定义群表示Group representation把群同态地映入向量空间可逆线性变换群的结构。2 个前置1 个后续
- 定义群的直积Direct product of groups在笛卡尔积上逐坐标定义运算得到的群。2 个前置1 个后续
- 定义群同态Group homomorphism保持群运算的映射,用于比较两个群的结构。2 个前置2 个后续
- 定义群作用Group action群元素以保持单位元与乘法的方式作用于集合。2 个前置5 个后续
- 定义商环Quotient ring按理想的陪集构造的环。2 个前置1 个后续
- 定义商模Quotient module按子模诱导的陪集等价关系取商并继承模运算的结构。3 个前置
- 定义商群Quotient group正规子群的陪集集合上诱导出的群。2 个前置3 个后续
- 定义商向量空间Quotient vector space按子空间诱导的陪集等价关系取商并继承向量运算的空间。3 个前置2 个后续
- 定义双线性映射与形式Bilinear map对两个向量变量分别线性的映射;值域为标量域时称双线性形式。2 个前置1 个后续
- 定义素理想Prime ideal商环为整环,等价地乘积落入该理想便至少有一因子落入其中的真理想。2 个前置
- 定义素元Prime element整除乘积时必整除至少一个因子的非零非单位元素。2 个前置4 个后续
- 定义特征多项式Characteristic polynomial由 det(λI−T) 定义并编码线性算子特征值的多项式。3 个前置
- 定义特征值与特征向量Eigenvalue and eigenvector满足 Tv=λv 且 v 非零的标量 λ 与向量 v。2 个前置2 个后续
- 定义外代数Exterior algebra把张量代数按 v⊗v=0 的关系取商所得的分次代数。2 个前置1 个后续
- 定义唯一分解整环Unique factorization domain每个非零非单位元素都能唯一地分解为不可约元乘积的整环。3 个前置
- 定义维数Dimension of a vector space向量空间任一基的基数。2 个前置1 个后续
- 定义线性无关Linear independence只有全零系数能产生零向量的向量组。1 个前置1 个后续
- 定义线性映射Linear map保持向量加法和标量乘法的函数。2 个前置8 个后续
- 定义线性组合与张成Linear combination and span有限标量加权和及由给定向量生成的最小子空间。2 个前置4 个后续
- 定义向量空间Vector space标量域作用下满足线性公理的加法阿贝尔群。2 个前置15 个后续
- 定义行列式Determinant对方阵给出标量并刻画体积缩放、可逆性和特征多项式的交替多线性函数。2 个前置5 个后续
- 定义循环群Cyclic group由单个元素的整数次幂生成的群。1 个前置1 个后续
- 定义幺半群Monoid具有双侧单位元的半群。1 个前置1 个后续
- 定义有限域Finite field底层集合有限的域。2 个前置2 个后续
- 定义域Field非零元素在乘法下均可逆的交换环。1 个前置7 个后续
- 定义域的特征Characteristic of a field单位元反复相加首次得到零的最小正整数,若不存在则为零。2 个前置1 个后续
- 定义域扩张Field extension一个域作为另一域子域时形成的包含关系与相应向量空间结构。2 个前置3 个后续
- 定义张量积Tensor product把双线性映射统一因子化为线性映射的向量空间构造。3 个前置1 个后续
- 定义整除Divisibility存在整数倍关系时定义的二元关系。1 个前置4 个后续
- 定义整环Integral domain含单位元 1≠0、无零因子的交换环。1 个前置5 个后续
- 定义正规子群Normal subgroup在群的共轭作用下保持不变的子群。1 个前置5 个后续
- 定义正合列Exact sequence相邻同态满足前一映像等于后一核的一列模与同态。2 个前置1 个后续
- 定义正交投影Orthogonal projection把向量映到子空间上最近点并使误差与子空间正交的线性算子。2 个前置
- 定义主理想整环Principal ideal domain每个理想都由单个元素生成的整环。2 个前置
- 定义子模Submodule对加法和标量乘法封闭的模子集。2 个前置1 个后续
- 定义子群Subgroup在原群运算下自身也构成群的非空子集。1 个前置6 个后续
- 定义自然变换Natural transformation由对象逐点态射组成并满足自然性方块交换的函子间映射。1 个前置2 个后续
- 定义自由模Free module具有基、因而每个元素可唯一写为有限线性组合的模。2 个前置
- 定义最大公约数Greatest common divisor同时整除两个整数且被所有公约数整除的非负整数。1 个前置3 个后续
- 定义Noether 环Noetherian ring每个理想有限生成,等价地理想升链最终稳定的环。2 个前置
- 模型群的呈示Group presentation用生成元集合和关系集合给出群的商结构描述。3 个前置1 个后续
- 模型线性方程组System of linear equations可写为矩阵方程 Ax=b 的有限个一次方程系统。2 个前置2 个后续
- 模型自由幺半群Free monoid由给定字母集合上的有限串及连接运算组成、满足相应泛性质的幺半群。2 个前置1 个后续
- 定理二次互反律Law of quadratic reciprocity把两个不同奇素数互为二次剩余的符号用一个精确的互反公式联系起来。1 个前置
- 定理费马小定理Fermat's little theorem素数 p 与不被 p 整除的整数 a 满足 a^(p−1)≡1 mod p。2 个前置
- 定理轨道–稳定子定理Orbit–stabilizer theorem有限群作用下元素轨道大小等于群阶除以稳定子阶。2 个前置
- 定理环上的中国剩余定理Chinese remainder theorem for rings两两互素理想的交商与对应商环直积之间存在规范同构。3 个前置
- 定理伽罗瓦理论基本定理Fundamental theorem of Galois theory有限伽罗瓦扩张的中间域与伽罗瓦群子群之间存在反序对应。3 个前置
- 定理拉格朗日定理Lagrange's theorem有限群中任意子群的阶整除原群的阶。3 个前置1 个后续
- 定理群第一同构定理First isomorphism theorem for groups群同态的定义域模核同构于其像。3 个前置
- 定理算术基本定理Fundamental theorem of arithmetic每个大于一的整数都能按次序无关且唯一地分解为素数乘积。3 个前置
- 定理有限生成阿贝尔群结构定理Structure theorem for finitely generated abelian groups每个有限生成阿贝尔群唯一分解为自由部分与有限循环素幂部分。2 个前置
- 定理有限维谱定理Finite-dimensional spectral theorem有限维实对称或复自伴算子存在正交规范特征向量基。3 个前置
- 定理整数中国剩余定理Chinese remainder theorem for integers两两互素模数下的同余方程组在模其乘积意义下有唯一解。2 个前置
- 定理秩–零化度定理Rank–nullity theorem有限维线性映射的定义域维数等于核维数与像维数之和。2 个前置
- 定理Cayley 定理Cayley's theorem每个群都同构于某个集合上的置换群的子群。2 个前置
- 定理Maschke 定理Maschke's theorem当域特征不整除有限群阶时,每个有限维表示都完全可约。3 个前置
- 定理Sylow 定理Sylow theorems描述有限群中素数幂阶子群的存在性、共轭性与数量约束。3 个前置
- 定理Yoneda 引理Yoneda lemma对象到一个函子的自然变换与该函子在对象处的元素自然双射。3 个前置
- 应用行化简Row reduction用初等行变换把矩阵化为阶梯形以求解线性方程组和判定秩。2 个前置
- 应用整数欧几里得算法Euclidean algorithm for integers反复使用带余除法计算最大公约数的有限算法。1 个前置
离散数学
组合计数、图、树与有限结构。
- 原则乘法原理Product rule分阶段且每阶段选择数固定时,总数等于各阶段选择数之积。3 个前置1 个后续
- 原则二阶矩方法Second moment method用方差或二阶矩控制随机变量偏离均值的概率。2 个前置
- 原则概率方法Probabilistic method通过证明随机选取对象具有正概率满足性质来推出确定性对象存在。2 个前置3 个后续
- 原则鸽巢原理Pigeonhole principle把多于 n 个对象放入 n 个容器时,至少一个容器包含两个对象。3 个前置2 个后续
- 原则隔板法Stars and bars把相同对象分入有标号盒子的整数解计数方法。2 个前置
- 原则加法原理Sum rule互斥有限选择类的总数等于各类大小之和。2 个前置
- 原则一阶矩方法First moment method用坏事件计数的期望小于一或 Markov 型界证明好对象存在。2 个前置
- 定义超图Hypergraph边可以连接任意多个顶点而非仅两个顶点的离散结构。2 个前置
- 定义错排Derangement没有任何元素停留在原位置的置换及其计数问题。2 个前置
- 定义递推关系Recurrence relation用先前项规定序列当前项的关系。2 个前置6 个后续
- 定义第二类 Stirling 数Stirling number of the second kind把 n 元集合划分为 k 个非空无标号块的方案数。2 个前置
- 定义顶点覆盖Vertex cover与每条边至少一个端点相交的顶点子集。2 个前置1 个后续
- 定义多项式系数Multinomial coefficient把 n 个可区分对象分入若干有标号组时的计数系数 n!/(n1!⋯nk!)。2 个前置
- 定义二分图Bipartite graph顶点可分成两部分且每条边跨越两部分的图。2 个前置3 个后续
- 定义二项式系数Binomial coefficientn 元集合的 k 元子集数,记作 C(n,k)。2 个前置2 个后续
- 定义分配格Distributive lattice交与并彼此满足分配律的格。1 个前置
- 定义割点与桥Cut vertex and bridge删除后增加连通分量数的顶点或边。1 个前置
- 定义格Lattice任意两元素都有最大下界与最小上界的偏序集。1 个前置1 个后续
- 定义集合划分Set partition把集合表示为两两不交非空块且其并为全体的块族。2 个前置2 个后续
- 定义阶乘Factorial前 n 个正整数的乘积 n!,并约定 0!=1。2 个前置1 个后续
- 定义链与反链Chain and antichain偏序集中任意两元素可比的子集与任意两不同元素不可比的子集。2 个前置1 个后续
- 定义路与圈Path and cycle in a graph由相邻顶点序列形成的路,以及首尾闭合的圈。2 个前置4 个后续
- 定义拟阵Matroid用遗传性和交换公理抽象线性无关集与森林结构的组合系统。2 个前置4 个后续
- 定义拟阵对偶Matroid duality以基的补集为基定义的对偶拟阵构造。2 个前置
- 定义欧拉迹Eulerian trail恰好一次经过每条边的迹。2 个前置
- 定义排列Permutation有限集合到自身的双射,或其元素的有序排列。2 个前置5 个后续
- 定义匹配Matching in a graph任意两条边都不共享端点的边集合。2 个前置4 个后续
- 定义平面图Planar graph可在平面中画出且边仅在共同端点相交的图。1 个前置2 个后续
- 定义普通生成函数Ordinary generating function把序列编码为形式幂级数 Σ a_n x^n。2 个前置1 个后续
- 定义区组设计Block design使每个小子集在固定数量区组中出现的均衡有限集合族。2 个前置
- 定义色数Chromatic number使图存在合法顶点着色所需的最少颜色数。2 个前置1 个后续
- 定义生成树Spanning tree包含原图全部顶点且自身为树的子图。2 个前置1 个后续
- 定义树Tree连通且不含环的无向图,等价地任意两点之间存在唯一简单路径。1 个前置9 个后续
- 定义图Graph用顶点集合和连接顶点对的边集合表示离散关系的结构。2 个前置23 个后续
- 定义图连通性Graph connectivity任意两顶点之间都存在路时图连通。2 个前置4 个后续
- 定义图染色Graph coloring把颜色赋给顶点并要求相邻顶点颜色不同。2 个前置1 个后续
- 定义完全图Complete graph任意两个不同顶点之间都有边的简单无向图。2 个前置
- 定义线性递推Linear recurrence relation当前项由固定数量先前项的线性组合给出。2 个前置
- 定义有限集Finite set与某个初始自然数段存在双射的集合。2 个前置40 个后续
- 定义有向图Directed graph边具有方向、可表示为顶点有序对集合的图。2 个前置3 个后续
- 定义整数分拆Integer partition把正整数写成若干正整数之和且忽略加数次序的表示。2 个前置
- 定义指数生成函数Exponential generating function以 a_n x^n/n! 编码带标号组合对象计数序列的形式幂级数。2 个前置
- 定义子图Subgraph顶点集和边集分别取原图子集且保持端点关系所得的图。2 个前置1 个后续
- 定义组合Combination从有限集合中无序选取固定数量元素所得的子集。3 个前置5 个后续
- 定义Catalan 数Catalan number计数正确括号串、凸多边形三角剖分等结构的一族整数。2 个前置
- 模型图拟阵Graphic matroid以图边为底集、以无环边集为独立集的拟阵。2 个前置
- 定理二项式定理Binomial theorem(x+y)^n 按二项式系数展开为各次幂项之和。2 个前置
- 定理拟阵贪心定理Matroid greedy theorem有限独立系统中,按非增权重加入可行元素对每个非负权重都产生最大权独立集,当且仅当该系统是拟阵。2 个前置1 个后续
- 定理偏序集 Möbius 反演Möbius inversion on posets在局部有限偏序集的区间和变换中用 Möbius 函数恢复原函数。3 个前置
- 定理平面图欧拉公式Euler's formula for planar graphs连通平面图的顶点数、边数与面数满足 V−E+F=2。2 个前置
- 定理容斥原理Inclusion–exclusion principle通过交集的交替和修正多个有限集合并集的重复计数。3 个前置1 个后续
- 定理Brooks 定理Brooks' theorem除完全图和奇环外,连通图色数不超过其最大度数。3 个前置
- 定理Burnside 引理Burnside's lemma有限群作用的轨道数等于各群元素不动点数的平均值。2 个前置1 个后续
- 定理Dilworth 定理Dilworth's theorem有限偏序集的最大反链大小等于覆盖全部元素所需的最少链数。2 个前置
- 定理Hall 婚配定理Hall's marriage theorem有限二分图存在饱和一侧的匹配,当且仅当每个该侧顶点子集的邻集至少同样大。3 个前置
- 定理Kőnig 二分图定理Kőnig's theorem for bipartite graphs二分图中最大匹配大小等于最小顶点覆盖大小。3 个前置
- 定理Kuratowski 定理Kuratowski's theorem有限图可平面嵌入,当且仅当不含 K5 或 K3,3 的细分子图。2 个前置
- 定理Lovász 局部引理Lovász local lemma当坏事件概率小且依赖稀疏时,所有坏事件同时不发生的概率为正。3 个前置
- 定理Pólya 枚举定理Pólya enumeration theorem用置换群的循环指标在对称作用下计数着色轨道。3 个前置
分析与概率
极限、连续性、测度与不确定性。
- 公理实数完备性Completeness of the real numbers每个非空且有上界的实数集合都存在最小上界。2 个前置3 个后续
- 公理Kolmogorov 概率公理Kolmogorov axioms用非负性、规范化和可列可加性定义概率测度。2 个前置17 个后续
- 原则拉格朗日乘子法Lagrange multiplier method约束极值处目标梯度位于约束梯度张成空间中的必要条件。2 个前置1 个后续
- 原则拉格朗日对偶Lagrange duality通过拉格朗日函数构造原问题下界的对偶问题,并研究弱对偶、强对偶与最优性条件。2 个前置1 个后续
- 定义测度Measure在 σ-代数上取非负扩展实值并满足可数可加性的函数。2 个前置4 个后续
- 定义导数Derivative函数增量比在步长趋零时的极限。2 个前置6 个后续
- 定义独立性Statistical independence联合事件概率等于各事件概率乘积的关系。2 个前置5 个后续
- 定义多元函数导数Derivative in several variables多元映射在一点的最佳线性近似。3 个前置9 个后续
- 定义方差Variance随机变量与其期望之差平方的期望。2 个前置3 个后续
- 定义分布函数Cumulative distribution function实值随机变量取值不超过 x 的概率作为 x 的非降右连续函数。2 个前置
- 定义复可微性Complex differentiability复差商在任意方向趋近时有同一极限的性质。3 个前置
- 定义复数Complex number形如 a+bi 的数,按坐标规则构成实数域的二次扩张。3 个前置1 个后续
- 定义赋范向量空间Normed vector space带满足正定、齐次与三角不等式范数的向量空间。2 个前置3 个后续
- 定义概率分布Probability distribution随机变量通过原像把样本空间概率推送到取值空间所得的概率测度。2 个前置10 个后续
- 定义概率密度函数Probability density function当概率分布对参考测度绝对连续时,其 Radon–Nikodym 密度。2 个前置
- 定义函数列一致收敛Uniform convergence of functions误差对定义域中所有点可由同一阶段统一控制的函数列收敛。3 个前置1 个后续
- 定义级数Infinite series序列各项的部分和序列及其极限。2 个前置4 个后续
- 定义级数绝对收敛Absolute convergence of series若各项绝对值组成的级数收敛,则原级数绝对收敛并必收敛。2 个前置1 个后续
- 定义极限Limit用任意精度的邻近关系描述序列或函数趋向某个值。1 个前置6 个后续
- 定义几乎必然收敛Almost sure convergence除去一个零概率事件后,随机变量序列逐样本收敛。2 个前置1 个后续
- 定义几乎处处Almost everywhere除去一个零测集后性质在其余所有点成立。2 个前置3 个后续
- 定义矩母函数Moment-generating function在存在邻域内以 E[e^{tX}] 编码随机变量各阶矩的函数。2 个前置
- 定义柯西序列Cauchy sequence任意精度下充分靠后的任意两项彼此接近的序列。2 个前置1 个后续
- 定义可测函数Measurable function使目标空间可测集的原像都属于定义域 σ-代数的函数。2 个前置3 个后续
- 定义可微性Differentiability函数在一点能被线性主部加高阶小量局部逼近的性质。2 个前置1 个后续
- 定义连续性Continuity函数在输入微小变化时输出可被控制为任意小变化的性质。1 个前置6 个后续
- 定义幂级数Power series形如 Σa_n(x−c)^n 并在收敛半径内定义函数的级数。2 个前置1 个后续
- 定义平衡点稳定性Stability of an equilibrium初值受到小扰动时轨道保持接近或最终回到平衡点的性质。2 个前置
- 定义平稳分布Stationary distribution经马尔可夫转移后保持不变的状态分布。2 个前置1 个后续
- 定义期望Expectation随机变量关于概率测度的积分。2 个前置11 个后续
- 定义弱导数Weak derivative通过分部积分恒等式相对于测试函数定义的广义导数。2 个前置1 个后续
- 定义上确界与下确界Supremum and infimum分别作为集合最小上界和最大下界的序结构元素。2 个前置2 个后续
- 定义随机变量Random variable从样本空间到可测数值空间的可测函数。3 个前置8 个后续
- 定义梯度Gradient标量函数微分在内积下对应的向量。2 个前置1 个后续
- 定义条件概率Conditional probability在已知正概率事件 B 时用 P(A∩B)/P(B) 更新事件 A 的概率。2 个前置2 个后续
- 定义条件期望Conditional expectation相对于子 σ-代数可测并保持其事件上积分的随机变量。3 个前置
- 定义凸函数Convex function函数在任意凸组合处不超过相同权重下函数值的凸组合。2 个前置1 个后续
- 定义凸集Convex set任意两点间线段全部包含在集合中的向量空间子集。2 个前置3 个后续
- 定义外测度Outer measure定义在所有子集上、取空集为零、单调且对可数并满足次可加不等式的集合函数。3 个前置
- 定义协方差Covariance两个随机变量中心化乘积的期望,衡量线性共同变化。2 个前置
- 定义序列Sequence以自然数为定义域的函数。2 个前置17 个后续
- 定义序列收敛Convergence of a sequence序列项最终任意接近某个极限值。2 个前置5 个后续
- 定义一致连续Uniform continuity同一 δ 对定义域中所有点同时控制给定 ε。2 个前置
- 定义依分布收敛Convergence in distribution分布函数在极限分布连续点处收敛的随机变量收敛概念。2 个前置2 个后续
- 定义依概率收敛Convergence in probability随机变量偏离极限超过任意正阈值的概率趋于零。2 个前置1 个后续
- 定义有界线性算子Bounded linear operator把有界集映为有界集,等价地连续的线性映射。2 个前置5 个后续
- 定义Banach 空间Banach space关于范数诱导度量完备的赋范向量空间。2 个前置3 个后续
- 定义Hilbert 空间Hilbert space由内积诱导范数且关于该范数完备的内积空间。2 个前置2 个后续
- 定义Jacobian 矩阵Jacobian matrix多元映射各偏导数组成并表示其导数的矩阵。2 个前置
- 定义L^p 空间L-p space对 1≤p≤∞,按几乎处处相等取商并配以 Lp 范数的可测函数空间。3 个前置1 个后续
- 定义Lebesgue 积分Lebesgue integral从简单函数积分出发按单调逼近扩展得到的积分。2 个前置8 个后续
- 定义Riemann 积分Riemann integral上下和或分割和在网格细化下共同收敛所定义的积分。3 个前置1 个后续
- 定义Sobolev 空间Sobolev space函数及若干阶弱导数都属于 Lp 的函数空间。2 个前置
- 定义σ-代数Sigma-algebra对补集和可数并封闭的子集族。3 个前置5 个后续
- 模型常微分方程Ordinary differential equation未知函数及其单一自变量导数组成的方程。2 个前置3 个后续
- 模型动力系统Dynamical system用时间演化映射或流描述状态空间轨道的系统。2 个前置1 个后续
- 模型偏微分方程Partial differential equation含未知多元函数及其偏导数的方程。2 个前置
- 模型实数系Real number system满足序域公理与上确界完备性的数系。3 个前置9 个后续
- 模型凸优化问题Convex optimization problem在凸可行域上最小化凸目标且不等式约束为凸函数的优化模型。2 个前置2 个后续
- 模型线性常微分方程组Linear system of ordinary differential equations形如 x′=A(t)x+b(t) 的向量值一阶线性方程组。2 个前置
- 模型Bernoulli 随机变量Bernoulli random variable只取 0 与 1 且成功概率为 p 的基本随机变量。2 个前置1 个后续
- 模型Markov 链Markov chain未来条件分布在给定当前状态后与更早历史无关的随机过程。2 个前置3 个后续
- 定理大数定律Law of large numbers独立同分布且可积时,样本均值几乎必然、因而依概率收敛到共同期望。4 个前置1 个后续
- 定理单调收敛定理Monotone convergence theorem非负可测函数单调递增时,积分极限等于极限函数积分。3 个前置
- 定理单调有界序列收敛定理Monotone convergence theorem for sequences每个单调且有界的实数序列都收敛。3 个前置
- 定理多元 Taylor 定理Multivariable Taylor theorem用各阶导数给出多元函数的局部多项式展开及余项控制。2 个前置
- 定理极值定理Extreme value theorem连续实值函数在非空紧空间上取得最大值和最小值。2 个前置
- 定理介值定理Intermediate value theorem连续实函数在区间上取得端点函数值之间的每个值。2 个前置
- 定理开映射定理Open mapping theoremBanach 空间之间的满射有界线性算子把开集映成开集。3 个前置
- 定理控制收敛定理Dominated convergence theorem几乎处处收敛且被同一可积函数控制时,可以交换极限与积分。3 个前置
- 定理马尔可夫链遍历定理Ergodic theorem for Markov chains不可约正常返链的时间平均趋于平稳平均;再加非周期性时转移分布趋于平稳分布。3 个前置
- 定理逆函数定理Inverse function theorem导数可逆的光滑映射在该点邻域内存在光滑局部逆。3 个前置1 个后续
- 定理泰勒定理Taylor's theorem足够光滑函数由有限阶导数多项式加余项表示。2 个前置1 个后续
- 定理微积分基本定理Fundamental theorem of calculus积分与求导在适当连续性条件下互为逆过程。3 个前置
- 定理一致有界原理Uniform boundedness principle一族有界线性算子若逐点有界,则其算子范数一致有界。2 个前置
- 定理隐函数定理Implicit function theorem当相关偏导块可逆时,方程组局部可把部分变量表示为其余变量的函数。2 个前置1 个后续
- 定理有界自伴算子谱定理Spectral theorem for bounded self-adjoint operatorsHilbert 空间上的有界自伴算子可由投影值测度或连续函数演算表示。2 个前置
- 定理中心极限定理Central limit theorem适当归一化的独立随机变量和在分布上趋于正态分布。4 个前置
- 定理中值定理Mean value theorem闭区间连续且内部可导的函数在某点导数等于割线斜率。2 个前置
- 定理Bayes 定理Bayes' theorem用先验概率和似然反转条件概率,得到观察证据后的后验概率。1 个前置1 个后续
- 定理Bolzano–Weierstrass 定理Bolzano–Weierstrass theorem实数空间中的每个有界序列都存在收敛子列。2 个前置
- 定理Borel–Cantelli 引理Borel–Cantelli lemmas由事件概率级数的收敛或在独立条件下的发散判断无限多事件发生概率。3 个前置
- 定理Fatou 引理Fatou's lemma非负可测函数列下极限的积分不超过积分的下极限。2 个前置
- 定理Fubini 定理Fubini's theorem在适当可积条件下,多重积分等于任意次序的迭代积分。3 个前置
- 定理Hahn–Banach 定理Hahn–Banach theorem在保持控制不等式或范数的条件下把子空间上线性泛函延拓到全空间。2 个前置
- 定理Hilbert 空间 Riesz 表示定理Riesz representation theorem for Hilbert spacesHilbert 空间上的每个连续线性泛函都唯一由与某向量取内积表示。2 个前置
- 定理Weierstrass M 判别法Weierstrass M-test若函数项被一个收敛数项级数逐项一致控制,则函数级数绝对且一致收敛。2 个前置
- 应用贝叶斯诊断推断Bayesian diagnostic inference把患病率、检测灵敏度和假阳性率组合为观察结果后的后验风险。1 个前置
几何与拓扑
距离、开集、连续变形与空间结构。
- 定义杯积Cup product使上同调成为分次环的自然双线性乘法。2 个前置
- 定义闭集Closed set补集为开集的集合。2 个前置4 个后续
- 定义测地线Geodesic局部保持平行速度并在短区间上实现长度驻值的曲线。2 个前置
- 定义道路连通空间Path-connected space任意两点可由从单位区间出发的连续路径连接。2 个前置1 个后续
- 定义第二可数空间Second-countable space存在可数拓扑基的拓扑空间。2 个前置
- 定义第一可数空间First-countable space每一点都有可数邻域基的拓扑空间。2 个前置
- 定义度量空间Metric space配备非负、对称并满足三角不等式的距离函数的集合。2 个前置6 个后续
- 定义仿射空间Affine space忘去原点但保留向量平移作用和仿射组合的空间。2 个前置2 个后续
- 定义覆叠空间Covering space连续满射在底空间每一点邻域上分解为若干互不相交的同胚片。3 个前置1 个后续
- 定义高斯曲率Gaussian curvature二维 Riemann 流形在一点截面曲率的内蕴标量。3 个前置1 个后续
- 定义光滑流形Smooth manifold坐标图之间转移映射光滑的拓扑流形。2 个前置3 个后续
- 定义积拓扑Product topology由有限坐标限制的基本开集生成的笛卡尔积拓扑。2 个前置1 个后续
- 定义基本群Fundamental group基点回路按端点固定同伦分类后形成的群。2 个前置1 个后续
- 定义紧化Compactification把空间同胚嵌入为某个紧 Hausdorff 空间的稠密子空间。4 个前置1 个后续
- 定义紧空间Compact space每个开覆盖都有有限子覆盖的空间。3 个前置6 个后续
- 定义局部紧空间Locally compact space每一点都有闭包紧的邻域的 Hausdorff 空间;等价地每点有紧邻域。3 个前置1 个后续
- 定义局部连通性Local connectedness每一点都有由连通开集组成的邻域基的性质。2 个前置
- 定义聚点Limit point每个邻域都含有集合中不同于该点的元素的点。2 个前置
- 定义开集Open set拓扑中被指定为开放的子集,是邻域、连续与内部的基本单位。1 个前置10 个后续
- 定义开球Open ball与中心距离小于给定正半径的全部点组成的集合。1 个前置
- 定义连通分支Connected component包含给定点的极大连通子集。2 个前置1 个后续
- 定义连通空间Connected space不能分成两个不交非空开集的空间。2 个前置2 个后续
- 定义邻域Neighborhood包含给定点的某个开集的集合。2 个前置5 个后续
- 定义流形定向Orientation of a manifold对各切空间一致选择正向基等价类的结构。2 个前置2 个后续
- 定义内部、闭包与边界Interior, closure, and boundary集合的最大开子集、最小闭超集及二者确定的边界。3 个前置
- 定义欧拉示性数Euler characteristic以胞腔交替计数或同调群秩交替和定义的拓扑不变量。2 个前置1 个后续
- 定义奇异单形Singular simplex标准单形到拓扑空间的连续映射。2 个前置1 个后续
- 定义奇异同调Singular homology以循环群对边界群取商得到的拓扑不变量。2 个前置3 个后续
- 定义切空间Tangent space在一点由曲线速度或函数导子等价定义的局部线性空间。2 个前置3 个后续
- 定义商拓扑Quotient topology使满射 q 连续的最细拓扑:U 开当且仅当 q⁻¹(U) 开。2 个前置
- 定义上同调Cohomology对链复形取到系数群的同态形成上链复形,再取上同调得到反变不变量。2 个前置1 个后续
- 定义射影空间Projective space把非零向量按非零标量倍数关系取商所得的直线空间。2 个前置
- 定义拓扑基Basis for a topology其任意并恰生成全部开集的局部开集族。2 个前置3 个后续
- 定义拓扑空间Topological space用开集族刻画邻近与连续结构,而不要求存在数值距离。2 个前置14 个后续
- 定义拓扑空间中的收敛Convergence in a topological space序列最终进入极限点每个邻域时定义的收敛。3 个前置
- 定义拓扑连续性Topological continuity开集的逆像仍为开集的映射,是不依赖距离的连续性定义。3 个前置9 个后续
- 定义拓扑流形Topological manifold局部同胚于欧氏空间且满足可数基与 Hausdorff 条件的空间。3 个前置1 个后续
- 定义同伦Homotopy在连续参数下把一个连续映射变形成另一个连续映射。2 个前置3 个后续
- 定义同胚Homeomorphism自身与逆映射都连续的双射。3 个前置4 个后续
- 定义外微分Exterior derivative把 k 形式映为 k+1 形式且满足 d²=0 与分次 Leibniz 规则的算子。2 个前置1 个后续
- 定义微分形式Differential form在每点切空间上光滑变化的交替多线性协变量场。2 个前置2 个后续
- 定义正规空间Normal space任意两个不交闭集都可由不交开集分离的拓扑空间。2 个前置2 个后续
- 定义子空间拓扑Subspace topology由母空间开集与子集相交得到的拓扑。3 个前置
- 定义Hausdorff 空间Hausdorff space任意两个不同点都可被不交开邻域分离的空间。2 个前置4 个后续
- 定义Riemann 度量Riemannian metric在每一点切空间上光滑变化的正定内积。3 个前置2 个后续
- 模型拓扑链复形Chain complex in topology由奇异单形生成的阿贝尔群与满足边界复合为零的边界算子组成。3 个前置2 个后续
- 模型同调正合列Exact sequence in homology空间对或链复形短正合列诱导的长正合群列。2 个前置1 个后续
- 模型Alexandroff 单点紧化Alexandroff one-point compactification向非紧局部紧 Hausdorff 空间添加一个无穷远点得到紧空间。2 个前置
- 定理度量诱导拓扑Metric topology度量空间的开球生成一个拓扑,把数值距离转化为纯拓扑结构。3 个前置
- 定理覆叠提升性质Lifting property for covering spaces路径与同伦在指定起点后可唯一提升到覆叠空间。3 个前置
- 定理流形上的 Stokes 定理Stokes' theorem on manifolds紧支撑微分形式的外微分在流形上的积分等于该形式在边界上的积分。3 个前置
- 定理同调的同伦不变性Homotopy invariance of homology同伦等价空间具有同构的奇异同调群。2 个前置
- 定理Brouwer 不动点定理Brouwer fixed-point theorem闭球到自身的任意连续映射都有不动点。3 个前置
- 定理Gauss–Bonnet 定理Gauss–Bonnet theorem闭定向曲面的总高斯曲率等于 2π 乘其欧拉示性数。4 个前置
- 定理Heine–Borel 定理Heine–Borel theorem欧氏空间子集紧致当且仅当它闭且有界。3 个前置
- 定理Jordan 曲线定理Jordan curve theorem平面中简单闭曲线的补集恰有内外两个连通分支且曲线是共同边界。3 个前置
- 定理Mayer–Vietoris 序列Mayer–Vietoris sequence用两个开子空间及其交的同调计算并集同调的长正合列。2 个前置
- 定理Seifert–van Kampen 定理Seifert–van Kampen theorem把空间开覆盖的基本群通过推送结构组合为整体基本群。3 个前置
- 定理Tietze 延拓定理Tietze extension theorem正规空间闭子集上的连续实值函数可连续延拓到全空间。3 个前置
- 定理Urysohn 引理Urysohn's lemma正规空间中两个不交闭集可被连续实值函数分别映到 0 与 1。2 个前置
理论计算机科学
279 条匹配自动机与可计算性
计算模型、语言、可判定性与不可计算性。
- 原则Church–Turing 论题Church–Turing thesis所有有效可计算过程都可由图灵机计算的经验性等价主张。1 个前置
- 定义部分函数Partial function只在定义域某个子集上赋值、允许部分输入无输出的函数。2 个前置1 个后续
- 定义部分可计算函数Partial computable function允许机器在函数未定义的输入上不停机的部分函数。2 个前置
- 定义可计算函数Computable function存在停机图灵机对每个定义域输入输出该函数值的函数。2 个前置1 个后续
- 定义可判定性Decidability存在对每个输入都停机并正确回答是或否的算法这一性质。1 个前置1 个后续
- 定义可识别语言Turing-recognizable language存在图灵机对语言内输入接受、对语言外输入可拒绝或不停机的语言。1 个前置2 个后续
- 定义文法歧义Grammar ambiguity某个字存在两个不同语法树或最左推导时文法具有的性质。2 个前置
- 定义形式语言Formal language字母表上有限字符串集合的抽象,是自动机输入与计算问题编码的基本对象。2 个前置13 个后续
- 定义映射归约Mapping reduction用可计算函数把一个语言成员关系变换为另一个语言成员关系。3 个前置1 个后续
- 定义余可识别语言Co-recognizable language补语言可被图灵机识别的语言。2 个前置
- 定义语言运算Language operations对语言进行并、交、补、连接与 Kleene 星等构造。2 个前置3 个后续
- 定义正则表达式Regular expression由空语言、空串、字符、并、连接和 Kleene 星有限构造的语言表达式。2 个前置2 个后续
- 定义正则语言Regular language能被某个有限自动机识别的形式语言。1 个前置3 个后续
- 定义字Word从某个有限位置集到字母表的函数,即有限符号序列。3 个前置13 个后续
- 定义字符串连接String concatenation把第二个字的符号接在第一个字之后形成的新字及相应结合运算。2 个前置
- 定义字母表Alphabet用于构造有限串的有限非空符号集合。2 个前置1 个后续
- 定义Brzozowski 导数Brzozowski derivative语言或正则表达式对首字符的剩余,表示读入给定前缀后仍可接受的后缀集合。2 个前置
- 定义Chomsky 范式Chomsky normal form除空字特殊规则外,每条产生式只形如 A→BC 或 A→a 的上下文无关文法标准形。1 个前置1 个后续
- 模型多带图灵机Multitape Turing machine具有固定有限条磁带和读写头但与单带模型可计算能力相同的机器。2 个前置
- 模型非确定性图灵机Nondeterministic Turing machine每个配置可有多个后继并在存在接受分支时接受的图灵机。2 个前置2 个后续
- 模型非确定性有限自动机Nondeterministic finite automaton转移可同时给出多个后继状态的有限状态机。2 个前置3 个后续
- 模型枚举器Enumerator machine按某种顺序打印语言中全部字且不打印外部字的图灵机变体。2 个前置
- 模型确定性下推自动机Deterministic pushdown automaton每个配置至多有一个可用转移且读入与 ε 转移不冲突的下推自动机。1 个前置
- 模型上下文无关文法Context-free grammar每条产生式左侧是单个非终结符的生成系统。2 个前置6 个后续
- 模型通用图灵机Universal Turing machine输入机器编码和输入串后模拟该机器运行的图灵机。2 个前置
- 模型图灵机Turing machine通过有限控制、可读写纸带和移动读写头刻画一般算法计算能力的模型。3 个前置17 个后续
- 模型下推自动机Pushdown automaton带无界栈存储的有限控制自动机。2 个前置2 个后续
- 模型有限自动机Finite automaton只有有限状态并逐符号读取输入的计算模型。3 个前置6 个后续
- 模型语法树Parse tree用树形结构记录文法产生式如何从开始符号生成一个字。2 个前置1 个后续
- 模型预言机图灵机Oracle Turing machine可在一步内查询某固定语言成员资格的相对可计算性模型。2 个前置1 个后续
- 模型Post 对应问题Post correspondence problem询问有限字符串牌集合是否存在上下串连接相等的非空序列。2 个前置
- 模型ε-NFAEpsilon-NFA允许不读取输入符号便改变状态的非确定性有限自动机。2 个前置
- 定理上下文无关语言泵引理Pumping lemma for context-free languages足够长的上下文无关语言词存在两个可同步泵送的片段。2 个前置
- 定理上下文无关语言闭包性质Closure properties of context-free languages上下文无关语言对并、连接、Kleene 星、同态和与正则语言求交封闭,但不对交和补封闭。2 个前置
- 定理停机问题不可判定性Halting problem不存在一个对任意程序和输入都能正确判断程序是否停机的算法。2 个前置
- 定理正则语言泵引理Pumping lemma for regular languages足够长的正则语言词可分解出可重复泵送的中段。3 个前置
- 定理正则语言闭包性质Closure properties of regular languages正则语言对并、交、补、连接、Kleene 星和逆同态等运算封闭。2 个前置
- 定理CFG–PDA 等价定理CFG–PDA equivalence上下文无关文法生成的语言恰为下推自动机接受的语言。2 个前置
- 定理DFA–NFA 等价定理DFA–NFA equivalence每个 NFA 都可由识别同一语言的 DFA 模拟。3 个前置
- 定理Kleene 定理Kleene's theorem正则表达式描述的语言恰为有限自动机识别的语言。3 个前置
- 定理Myhill–Nerode 定理Myhill–Nerode theorem语言正则当且仅当其右同余等价类有限,且类数等于最小 DFA 状态数。2 个前置1 个后续
- 定理Rice 定理Rice's theorem图灵可识别语言的每个非平凡语义性质都是不可判定的。2 个前置
- 应用有限自动机最小化Finite automaton minimization合并不可区分状态以得到识别同一语言且状态数最少的 DFA。3 个前置
- 应用CYK 算法Cocke–Younger–Kasami algorithm用区间动态规划判定给定字是否属于 Chomsky 范式文法生成的语言。3 个前置
计算复杂性
资源界、复杂度类与问题归约。
- 原则概率放大Probability amplification独立重复并多数表决可把有界错误概率指数降低。2 个前置
- 定义参数化复杂度类 FPTFixed-parameter tractable可在 f(k)n^O(1) 时间内求解的参数化问题类。2 个前置
- 定义参数化问题Parameterized problem实例与非负整数参数共同组成的判定问题。2 个前置1 个后续
- 定义电路规模与深度Circuit size and depth分别计数门数和最长输入到输出路径长度的电路资源度量。2 个前置1 个后续
- 定义电路族一致性Circuit family uniformity要求输入长度 n 对应电路可由统一算法有效生成的条件。3 个前置1 个后续
- 定义多项式层级Polynomial hierarchy由交替存在和全称多项式证书或逐层 NP 预言机构成的复杂性层级。3 个前置
- 定义多项式时间归约Polynomial-time reduction用一个多项式时间可计算的变换把问题 A 的实例转换为问题 B 的实例。3 个前置2 个后续
- 定义多项式时间近似方案Polynomial-time approximation scheme对每个固定 ε>0 都在多项式时间内给出 1±ε 近似的算法族。2 个前置
- 定义非确定性空间复杂性类Nondeterministic space class由非确定性图灵机在给定空间界内判定的语言集合。3 个前置
- 定义非确定性时间复杂性类Nondeterministic time class由非确定性图灵机在给定时间界内判定的语言集合。3 个前置
- 定义复杂度类 BPPComplexity class BPP具有有界双边误差多项式时间随机算法的语言类。2 个前置1 个后续
- 定义复杂度类 coNPComplexity class co-NP补语言属于 NP 的语言类。2 个前置1 个后续
- 定义复杂度类 LComplexity class L可在确定性对数空间内判定的语言类。1 个前置
- 定义复杂度类 NLComplexity class NL可在非确定性对数空间内判定的语言类。1 个前置1 个后续
- 定义复杂度类 NPNP是实例拥有可在多项式时间内验证的多项式长度证明的语言集合。1 个前置5 个后续
- 定义复杂度类 PP能由确定性算法在输入长度的多项式时间内判定的语言集合。1 个前置
- 定义复杂度类 PSPACEComplexity class PSPACE可由确定性图灵机在多项式空间内判定的语言类。1 个前置
- 定义复杂度类 RPComplexity class RP具有单边误差多项式时间随机算法的语言类。2 个前置
- 定义复杂性类 EXPEXPTIME可由确定性图灵机在单指数时间内判定的语言类。2 个前置
- 定义复杂性类 NCNick's Class由多项式规模、复对数深度的统一布尔电路族判定的高度并行语言类。3 个前置
- 定义近似比Approximation ratio近似算法解值与最优值之间的最坏情形乘法保证。1 个前置1 个后续
- 定义空间复杂度Space complexity计算在输入长度函数下使用的工作存储单元数量。2 个前置6 个后续
- 定义确定性空间复杂性类Deterministic space class由确定性图灵机在给定工作空间界内判定的语言集合。3 个前置1 个后续
- 定义确定性时间复杂性类Deterministic time class由确定性图灵机在给定时间界内判定的语言集合。3 个前置1 个后续
- 定义时间复杂度Time complexity算法或计算模型在输入规模增长时所需基本步骤数量的渐近上界。2 个前置11 个后续
- 定义NP 困难性NP-hardnessNP 中每个语言都可多项式时间归约到目标问题。2 个前置1 个后续
- 定义NP 完全性NP-completeness同时属于 NP 且为 NP-hard 的性质。2 个前置1 个后续
- 模型3-SAT3-SAT每个子句恰含三个文字的合取范式可满足性问题。1 个前置1 个后续
- 模型布尔电路Boolean circuit由逻辑门构成的有限无环有向图,计算布尔函数。2 个前置3 个后续
- 定理顶点覆盖 NP 完全性NP-completeness of Vertex Cover判定图是否存在大小至多 k 的顶点覆盖是 NP 完全问题。3 个前置
- 定理空间层级定理Space hierarchy theorem在适当空间可构造性条件下,更多渐近空间严格提升可判定语言能力。3 个前置
- 定理时间层级定理Time hierarchy theorem在可构造时间界下,给予更多渐近时间会严格扩大可判定语言类。2 个前置
- 定理Cook–Levin 定理Cook–Levin theorem布尔可满足性问题 SAT 是 NP 完全问题。2 个前置
- 定理Savitch 定理Savitch's theorem对适当空间函数 s,NSPACE(s) 包含于 DSPACE(s²)。2 个前置
算法与数据结构
正确性、效率、设计范式与信息组织。
- 原则递归式代入法Substitution method for recurrences先猜测渐近界再用归纳代入验证并调节常数的方法。3 个前置
- 原则递归树法Recursion-tree method把递归式各层代价展开成树并对层和叶子求和的渐近分析方法。2 个前置
- 原则动态规划Dynamic programming利用重叠子问题和最优子结构缓存递推结果的设计范式。1 个前置4 个后续
- 原则分治法Divide and conquer把问题分成较小同类子问题,递归求解后合并结果的算法设计范式。4 个后续
- 原则回溯法Backtracking深度优先枚举部分解并在不可能完成时撤销选择的搜索范式。2 个前置
- 原则记忆化Memoization缓存递归子问题结果以避免重复计算的自顶向下动态规划技术。2 个前置
- 原则势能法Potential method用数据结构状态势能的变化修正实际成本以界定均摊成本。2 个前置
- 原则贪心算法Greedy algorithm每一步作局部最优且不回溯选择的算法设计范式。7 个后续
- 原则摊还分析Amortized analysis对操作序列的总成本作上界,而非逐次最坏成本。2 个前置1 个后续
- 原则循环不变式Loop invariant在循环初始化后成立、每轮保持,并与终止条件共同推出结果的断言。1 个前置
- 原则原始—对偶方法Primal-dual method同时维护原问题与对偶问题的可行性和互补条件以构造解的算法框架。2 个前置
- 定义渐近记号Asymptotic notation忽略常数和低阶项,比较函数在输入趋于无穷时增长速度的记号体系。2 个前置11 个后续
- 定义平衡搜索树Balanced search tree以结构不变量保证对数高度和最坏对数搜索时间的二叉搜索树族。2 个前置1 个后续
- 定义顺序统计量Order statistic有限有序样本排序后第 k 个位置的元素。2 个前置
- 定义算法正确性Algorithm correctness算法对所有满足前置条件的输入都满足规格,并在完全正确时保证终止。5 个后续
- 定义凸包Convex hull包含给定点集的最小凸集及其计算问题。2 个前置
- 定义有向无环图Directed acyclic graph不含有向环的有向图。2 个前置1 个后续
- 模型比较排序Comparison sorting仅通过元素两两比较确定排列次序的排序模型。2 个前置4 个后续
- 模型并查集Disjoint-set union维护不交集合划分并支持合并与代表元查询的数据结构。2 个前置1 个后续
- 模型抽象数据类型Abstract data type由值集合与操作语义定义、独立于具体表示的数据接口。2 个前置7 个后续
- 模型队列Queue在尾部插入、头部删除、遵循先进先出的结构。2 个前置1 个后续
- 模型二叉堆Binary heap以近完全二叉树表示并满足父子堆序的优先队列结构。3 个前置1 个后续
- 模型二叉树Binary tree每个节点至多有两个有序子节点的根树。1 个前置1 个后续
- 模型二叉搜索树Binary search tree每个结点左子树键小于、右子树键大于该结点键的二叉树。2 个前置2 个后续
- 模型二分查找Binary search在有序数组中反复排除一半候选区间的查找算法。2 个前置
- 模型广度优先搜索Breadth-first search按无权距离分层访问可达顶点的图遍历算法。3 个前置1 个后续
- 模型归并排序Merge sort递归排序两半并线性合并的稳定比较排序算法。3 个前置
- 模型哈希表Hash table用哈希函数把键映射到桶并处理冲突的字典结构。2 个前置
- 模型红黑树Red-black tree用节点颜色和路径黑高不变量保持近似平衡的二叉搜索树。2 个前置
- 模型后缀数组Suffix array按字典序排列字符串全部后缀起始位置的数组索引。3 个前置
- 模型计算几何问题Computational geometry problem以点、线段、多边形等几何对象为输入并要求组合或数值几何输出的问题族。2 个前置
- 模型快速排序Quicksort围绕枢轴分区后递归排序子数组的比较排序算法。2 个前置
- 模型链表Linked list节点通过指针连接并支持局部插入删除的线性数据结构。2 个前置
- 模型深度优先搜索Depth-first search沿未访问边尽可能深入后回溯的图遍历算法。3 个前置2 个后续
- 模型数组Array以连续整数下标支持随机访问的有限序列结构。2 个前置9 个后续
- 模型随机化算法Randomized algorithm把随机比特作为额外输入并分析输出正确率或运行时间分布的算法。2 个前置3 个后续
- 模型拓扑排序Topological sort给有向无环图顶点排列线性次序,使每条边从前指向后。2 个前置
- 模型线性规划Linear programming在线性等式和不等式约束下优化线性目标函数的问题。2 个前置3 个后续
- 模型优化问题Optimization problem在可行解集合上最小化或最大化目标函数的计算问题。3 个前置2 个后续
- 模型栈Stack只在同一端插入和删除、遵循后进先出的结构。2 个前置2 个后续
- 模型字典树Trie按字符串前缀共享路径组织键集合的树形数据结构。2 个前置
- 模型字符串匹配String matching在文本中定位模式串全部出现位置的问题。2 个前置2 个后续
- 模型最大流Maximum flow在容量与流守恒约束下最大化源到汇净流量的问题。3 个前置5 个后续
- 模型最短路问题Shortest-path problem在带边代价图中寻找两点之间总代价最小路径的问题。2 个前置3 个后续
- 模型最小费用流Minimum-cost flow在满足流量守恒与容量限制下最小化边费用总和的网络优化问题。2 个前置
- 模型最小生成树Minimum spanning tree连通加权图中总边权最小的生成树及其算法问题。3 个前置2 个后续
- 模型Dijkstra 算法Dijkstra's algorithm在非负边权图中逐次确定最短距离的单源最短路算法。2 个前置
- 定理比较排序下界Comparison sorting lower bound任何最坏情形比较排序都需 Ω(n log n) 次比较。3 个前置
- 定理主定理Master theorem比较递归子问题总量与合并成本,快速求解一类分治递推式的渐近界。2 个前置
- 定理最大流最小割定理Max-flow min-cut theorem网络最大流值等于源汇最小割容量。2 个前置
- 应用单纯形法Simplex method沿可行多面体顶点与边枢轴移动求解线性规划的方法。2 个前置
- 应用方向判定Orientation test用二维或高维行列式符号判断点组转向或仿射定向的基本谓词。2 个前置
- 应用基数排序Radix sort按稳定子程序逐位处理固定长度键的非比较排序。2 个前置
- 应用计数排序Counting sort对有限整数键频数计数并按前缀位置输出的线性时间非比较排序。3 个前置1 个后续
- 应用经由网络流的二分图匹配Bipartite matching via maximum flow把二分图匹配编码为单位容量流网络并由最大流恢复匹配。3 个前置
- 应用拟阵贪心算法Matroid greedy algorithm按权重依次加入仍保持独立的元素以求最大权拟阵基的算法。3 个前置
- 应用强连通分量算法Strongly connected components algorithm在线性时间内把有向图划分为互相可达的极大顶点集合。3 个前置
- 应用匈牙利算法Hungarian algorithm通过对偶标号和增广结构求解赋权二分图完美匹配的算法。3 个前置
- 应用选择算法Selection algorithm在未排序序列中求第 k 小元素而无需完全排序的算法族。3 个前置
- 应用Bellman–Ford 算法Bellman–Ford algorithm通过反复松弛边求含负权边图的单源最短路并检测可达负环。3 个前置
- 应用Dinic 算法Dinic's algorithm分层残量网络上反复计算阻塞流的最大流算法。3 个前置
- 应用Floyd–Warshall 算法Floyd–Warshall algorithm以允许的中间顶点集合为阶段计算全部顶点对最短路。3 个前置
- 应用Ford–Fulkerson 方法Ford–Fulkerson method沿残量网络中的增广路反复增加流量直至不存在增广路。2 个前置
- 应用KMP 算法Knuth–Morris–Pratt algorithm利用模式自身前后缀信息避免文本指针回退的线性时间字符串匹配算法。2 个前置
- 应用Kruskal 算法Kruskal's algorithm按边权递增加入不成环边并用并查集维护连通分量的最小生成树算法。3 个前置
- 应用Prim 算法Prim's algorithm从一个顶点开始反复加入跨越当前割的最轻边的最小生成树算法。3 个前置
- 应用Rabin–Karp 算法Rabin–Karp algorithm用滚动指纹筛选候选位置并核验相等性的字符串匹配算法。3 个前置
程序语言与类型论
语法、语义、类型系统与证明对应。
- 原则Curry–Howard 对应Curry–Howard correspondence把命题对应为类型、证明对应为程序、证明化简对应为程序求值。2 个前置
- 定义变量绑定Variable binding语法中的绑定出现将变量使用关联到其作用域内声明。2 个前置1 个后续
- 定义参数多态Parametric polymorphism程序对类型参数统一工作而不依赖其具体表示的多态。1 个前置2 个后续
- 定义递归类型Recursive type通过类型方程把类型变量递归绑定到包含自身的类型。1 个前置
- 定义多步归约Multi-step reduction单步归约关系的自反传递闭包,用于表达零步或有限多步执行。2 个前置
- 定义和类型Sum type其值从若干带标签分支中选择一个的类型。1 个前置1 个后续
- 定义积类型Product type其值由两个分量组成并支持投影的类型。2 个前置
- 定义类型判断Typing judgment在上下文中断言项具有某类型的形式判断。2 个前置8 个后续
- 定义求值上下文Evaluation context带单个洞的语法结构,用来确定下一步可归约子项的位置。2 个前置3 个后续
- 定义无捕获替换Capture-avoiding substitution把项代入自由变量时通过重命名避免自由变量被意外绑定。2 个前置1 个后续
- 定义续延Continuation表示计算余下部分、接收当前结果并产生最终结果的对象。2 个前置
- 定义依赖类型Dependent type类型表达式可依赖项值的类型系统构造。2 个前置
- 定义正规化性质Normalization property每个良构或良类型项能否经有限归约到正规形的性质。2 个前置1 个后续
- 定义子类型Subtyping允许某类型值在期望其上界类型的位置使用的可替代关系。2 个前置
- 定义最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。2 个前置
- 定义Hoare 三元组Hoare triple断言若前置条件成立且程序终止,则后置条件成立的 {P}C{Q} 形式。2 个前置3 个后续
- 定义α-等价Alpha-equivalence仅对绑定变量作一致改名而得到的项视为等价。2 个前置1 个后续
- 定义β-归约Beta reduction把函数抽象应用于实参时用无捕获替换消去应用的核心归约规则。2 个前置2 个后续
- 定义λ-正规形Lambda normal form不含任何 β-可约表达式的 λ 项。1 个前置1 个后续
- 模型操作语义Operational semantics用抽象机器或逐步归约关系定义程序如何执行。1 个前置6 个后续
- 模型抽象语法树Abstract syntax tree以树结构保留程序构造层次而省略表面语法细节的表示。2 个前置3 个后续
- 模型传名调用Call by name把尚未求值的实参表达式直接替入函数体且只在需要时展开的策略。2 个前置
- 模型传值调用Call by value仅当实参先求值为值后才进行函数体替换的求值策略。2 个前置
- 模型大步语义Big-step semantics用表达式直接求值到最终结果的归纳判断描述程序执行。2 个前置
- 模型分离逻辑Separation logic以分离合取表达互不重叠资源并局部推理堆内存的程序逻辑。2 个前置1 个后续
- 模型公理语义Axiomatic semantics用逻辑断言和推理规则描述程序状态变换性质的语义方法。2 个前置1 个后续
- 模型简单类型 λ 演算Simply typed lambda calculus给 λ 演算加入基础类型与函数类型,从语法上排除一类无意义应用。1 个前置4 个后续
- 模型可变状态语义Semantics of mutable state把位置到值的存储纳入配置并随求值更新的语义。2 个前置1 个后续
- 模型小步操作语义Small-step operational semantics用配置之间的一步转移关系及其反身传递闭包描述程序求值。2 个前置4 个后续
- 模型异常语义Exception semantics把正常返回与异常传播作为不同控制结果描述的语义。2 个前置
- 模型指称语义Denotational semantics把程序构造组合地解释为数学对象与函数的语义方法。1 个前置
- 模型Hindley–Milner 类型推断Hindley–Milner type inference为 let 多态 λ 项推导主类型的约束求解体系。2 个前置
- 模型System FSystem F具有显式类型抽象与类型应用的二阶多态 λ 演算。2 个前置
- 模型λ 演算Lambda calculus只用变量、函数抽象和函数应用表达计算的极简形式系统。4 个后续
- 定理简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个有类型的简单 λ 项的所有 β-归约序列都有限并到达正规形。2 个前置
- 定理进展与保持定理Progress and preservation良类型闭项不会卡住,并且求值步骤不会改变其类型。2 个前置
- 定理框架规则Frame rule若命令不修改额外资源,则可把该资源同时附加到前置和后置断言。2 个前置
- 定理Church–Rosser 定理Church–Rosser theorem若同一 λ 项可归约到两个结果,则二者还能归约到共同项。2 个前置
信息与密码学
信息量、编码、安全定义与密码构造。
- 原则混合论证Hybrid argument在一串相邻实验间逐步替换组件并累加不可区分优势的证明方法。2 个前置
- 定义不可区分性Computational indistinguishability任意高效判别器区分两个分布族的优势都是可忽略量。3 个前置1 个后续
- 定义单向函数One-way function易于正向计算但对随机输入像难以由任何高效算法求出原像的函数族。3 个前置
- 定义典型集Typical set长随机序列中概率与 2^{-nH} 同阶且总概率趋近一的序列集合。3 个前置
- 定义互信息Mutual information一个随机变量对另一个随机变量不确定性的平均减少量。2 个前置3 个后续
- 定义计算安全Computational security仅要求任何资源受限攻击者的成功优势足够小的安全概念。3 个前置11 个后续
- 定义交叉熵Cross-entropy在真实分布下对另一分布负对数似然取期望所得的信息量。3 个前置
- 定义抗碰撞性Collision resistance高效对手找到两个不同输入具有相同哈希值的概率可忽略。2 个前置
- 定义可忽略函数Negligible function比任意逆多项式最终更小的非负函数。2 个前置6 个后续
- 定义联合熵Joint entropy随机变量元组不确定性的 Shannon 熵。2 个前置1 个后续
- 定义率失真函数Rate-distortion function在允许期望失真不超过 D 时,所有重构信道互信息的下确界。3 个前置
- 定义签名不可伪造性Existential unforgeability under chosen-message attack即使可查询所选消息签名,高效对手也难为新消息产生有效签名的安全定义。2 个前置
- 定义前缀码Prefix-free code任一码字都不是另一不同码字前缀的可即时译码编码。2 个前置2 个后续
- 定义条件熵Conditional entropy已知一个随机变量后另一个随机变量剩余不确定性的平均值。1 个前置2 个后续
- 定义完美保密Perfect secrecy对每种消息先验,观察密文都不改变消息分布的无条件安全定义。1 个前置1 个后续
- 定义线性码Linear code有限域向量空间中的线性子空间作为码字集合的信道码。3 个前置3 个后续
- 定义信道容量Channel capacity对输入分布最大化输入与输出互信息所得的每次使用信息率。2 个前置1 个后续
- 定义选择密文安全Chosen-ciphertext attack security对手还可查询非挑战密文解密时仍保持消息不可区分的安全定义。2 个前置
- 定义选择明文安全Chosen-plaintext attack security对手可自适应查询所选明文加密时仍不能区分挑战消息的安全定义。2 个前置2 个后续
- 定义语义安全Semantic security密文不让多项式时间攻击者显著获得明文任何可计算信息的安全性。2 个前置1 个后续
- 定义Hamming 距离Hamming distance两个等长字在对应位置不同的坐标数。2 个前置1 个后续
- 定义KL 散度Kullback–Leibler divergence分布 P 相对于 Q 的对数似然比期望。2 个前置
- 定义Shannon 熵Shannon entropy随机变量不确定性的平均信息量,以最优编码所需位数为基本解释。1 个前置7 个后续
- 模型安全多方计算Secure multiparty computation多方在不泄露各自私有输入的情况下共同计算函数。2 个前置
- 模型承诺方案Commitment scheme由承诺和打开两个阶段组成并满足隐藏性与绑定性的密码协议。2 个前置
- 模型对称加密Symmetric encryption发送方与接收方共享密钥的加密、解密算法体系。2 个前置4 个后续
- 模型二元对称信道Binary symmetric channel每个输入比特以固定交叉概率独立翻转的二元信道。2 个前置
- 模型分组密码Block cipher由密钥索引固定长度消息空间上的可逆置换族。2 个前置
- 模型公钥加密Public-key encryption加密密钥公开而解密密钥保密的加密体系。2 个前置1 个后续
- 模型离散无记忆信道Discrete memoryless channel每次输出只依赖当前输入且各次使用条件独立的有限字母信道。2 个前置2 个后续
- 模型零知识证明Zero-knowledge proof证明者使验证者相信陈述为真而不泄露额外知识的交互证明。2 个前置
- 模型流密码Stream cipher把短密钥扩展为伪随机密钥流并与明文逐位组合的加密方式。2 个前置
- 模型秘密共享Secret sharing把秘密分成份额,使授权集合可恢复而非授权集合不获信息。2 个前置
- 模型密码哈希函数Cryptographic hash function把任意长输入压缩到固定长度并要求原像、第二原像或碰撞难求的函数族。3 个前置1 个后续
- 模型认证加密Authenticated encryption同时提供机密性与密文完整性的对称加密接口和安全目标。3 个前置
- 模型数字签名Digital signature由私钥签名、公开验证并提供不可伪造性的认证机制。2 个前置1 个后续
- 模型伪随机函数Pseudorandom function由短密钥索引且对高效查询者不可与真随机函数区分的函数族。2 个前置1 个后续
- 模型伪随机生成器Pseudorandom generator把短均匀种子扩展为计算上不可与均匀串区分的长输出。3 个前置1 个后续
- 模型消息认证码Message authentication code用共享密钥生成并验证消息完整性标签的机制。2 个前置1 个后续
- 模型信道码Channel code把消息映为信道输入码字并从带噪输出恢复消息的编码—译码对。2 个前置2 个后续
- 模型信源码Source code把信源符号或符号块映为码字以便无失真或有失真表示的编码。3 个前置1 个后续
- 模型一次一密One-time pad使用与消息等长的均匀随机密钥并只使用一次的异或加密方案。2 个前置
- 模型Diffie–Hellman 密钥交换Diffie–Hellman key exchange双方公开交换群幂并在离散对数型假设下导出共享秘密的协议。2 个前置
- 模型Reed–Solomon 码Reed–Solomon code以低次数多项式在互异域元素处的取值向量形成的最大距离可分码。3 个前置
- 定理渐近等分性质Asymptotic equipartition property离散无记忆源的长序列每符号信息量几乎必然收敛到熵。2 个前置1 个后续
- 定理数据处理不等式Data processing inequality对 Markov 链 X→Y→Z,有 I(X;Z)≤I(X;Y)。2 个前置
- 定理完美保密密钥下界Shannon key-length bound在正确且完美保密的系统中,密钥熵不能小于消息熵。2 个前置
- 定理无噪声编码定理Source coding theorem独立同分布信源的无损压缩平均码率可以逼近但不能低于其熵。1 个前置
- 定理有噪信道编码定理Noisy-channel coding theorem低于离散无记忆信道容量的速率可实现任意小错误概率,而高于容量的速率不能可靠传输。2 个前置
- 定理Fano 不等式Fano's inequality用估计错误概率上界条件熵,从而把信息不足转化为推断下界。2 个前置
- 定理Hamming 界Hamming bound由互不相交纠错球的体积给出码大小、长度与最小距离的上界。3 个前置
- 定理Kraft–McMillan 不等式Kraft–McMillan inequality刻画给定码长集合存在前缀码或唯一可译码的必要充分不等式。2 个前置
- 应用综合译码Syndrome decoding用校验矩阵计算接收向量综合并选择相应陪集首领纠错的译码方法。3 个前置
- 应用Huffman 编码Huffman coding反复合并最低概率符号构造期望码长最小前缀码的算法。3 个前置
并发与分布式系统
事件顺序、一致性、共识与故障边界。
- 原则安全性与活性Safety and liveness把系统正确性分为坏事永不发生与好事最终发生两类性质。1 个前置6 个后续
- 定义分布式共识Distributed consensus多个进程在可能故障和通信延迟下对一个值达成一致的任务。1 个前置5 个后续
- 定义分布式配置Distributed configuration全部进程局部状态与通信介质状态组成的系统全局状态。2 个前置1 个后续
- 定义互斥Mutual exclusion临界区任意时刻至多容纳一个进程;完整问题通常另规定进入进展条件。2 个前置
- 定义可串行化Serializability并发事务历史与某个串行事务次序等价的正确性条件。1 个前置
- 定义可容许执行Admissible execution满足给定调度、公平性和故障模型约束的执行。3 个前置1 个后续
- 定义顺序一致性Sequential consistency所有操作可排成保持各进程程序顺序的单一顺序历史。3 个前置
- 定义网络分区Network partition通信链路故障使进程网络分裂为暂时无法互达的多个连通部分。2 个前置1 个后续
- 定义无锁进展Lock-free progress系统整体保证在有限步内有某个操作完成,而不保证指定线程。2 个前置
- 定义线性一致性Linearizability每次操作可放置在调用与返回之间的单点,使历史等价于满足实时顺序的顺序规范。3 个前置1 个后续
- 定义原子操作Atomic operation对并发观察者不可分割、可视为在单一瞬间完成的操作。2 个前置2 个后续
- 定义执行历史Execution history按调用、返回、发送、接收或内部步骤记录系统事件的有限或无限序列。2 个前置5 个后续
- 定义最终一致性Eventual consistency停止更新后,所有副本最终收敛到一致状态的弱一致性保证。2 个前置1 个后续
- 定义Happens-before 关系Happens-before由进程内顺序与消息传递生成的事件因果偏序。1 个前置2 个后续
- 模型拜占庭故障Byzantine failure故障进程可任意偏离协议并向不同接收者发送矛盾信息。1 个前置2 个后续
- 模型拜占庭可靠广播Byzantine reliable broadcast即使发送者或接收者存在拜占庭故障,正确进程仍满足一致交付性质的广播原语。2 个前置
- 模型崩溃故障Crash failure进程停止执行且此后不再采取步骤的故障。1 个前置6 个后续
- 模型比较并交换Compare-and-swap原子地比较内存值并在相等时写入新值、同时返回比较结果的读改写原语。2 个前置
- 模型并发对象Concurrent object可被多个线程并发调用并以顺序规格解释操作效果的共享对象。3 个前置2 个后续
- 模型读改写原语Read-modify-write operation在单个原子步骤中读取旧值、计算并写入新值的共享内存操作。2 个前置
- 模型共享内存系统Shared-memory system进程通过读写共享对象交互的并发模型。2 个前置5 个后续
- 模型故障检测器Failure detector为进程提供关于其他进程是否故障的可能不可靠怀疑信息的抽象。2 个前置
- 模型可靠广播Reliable broadcast保证有效性、一致性和完整性的广播抽象。3 个前置4 个后续
- 模型两阶段提交Two-phase commit协调者先收集准备结果再统一决定提交或中止的原子提交协议。2 个前置
- 模型逻辑时钟Logical clock为事件赋整数时间戳并保证因果先后蕴含时间戳递增。2 个前置1 个后续
- 模型实用拜占庭容错Practical Byzantine Fault Tolerance在部分同步网络与至多 f 个拜占庭副本下使用 3f+1 副本实现状态机复制的协议。3 个前置
- 模型视图戳复制Viewstamped Replication用视图变更和主副本日志在崩溃故障下复制状态机的协议。3 个前置
- 模型同步系统Synchronous distributed system计算步和通信延迟有已知上界的系统模型。2 个前置
- 模型无冲突复制数据类型Conflict-free replicated data type通过单调状态合并或可交换操作在无协调下保证副本收敛的数据类型。2 个前置
- 模型向量时钟Vector clock用每进程计数向量在标准消息传递模型中精确刻画事件因果偏序。2 个前置1 个后续
- 模型消息传递系统Message-passing system进程仅通过发送和接收消息交互的分布式模型。2 个前置6 个后续
- 模型选主问题Leader election使所有正确进程最终一致输出同一唯一进程为领导者的分布式任务。3 个前置2 个后续
- 模型异步系统Asynchronous distributed system消息延迟和进程相对速度没有已知有限上界的系统模型。1 个前置5 个后续
- 模型因果广播Causal broadcast保证所有进程按因果先后顺序交付消息的广播抽象。3 个前置
- 模型原子广播Atomic broadcast所有正确进程以同一总序交付广播消息。2 个前置1 个后续
- 模型状态机State machine用状态集合、初始状态和转移关系描述系统可能执行轨迹的模型。2 个前置13 个后续
- 模型PaxosPaxos consensus在多数法定人数与稳定领导等条件下实现崩溃容错共识的协议族。3 个前置
- 模型Raft 共识协议Raft consensus algorithm以任期、选主和复制日志实现崩溃容错共识的协议。3 个前置
- 定理共识与原子广播等价性Equivalence of consensus and atomic broadcast在标准故障模型下,共识可实现原子广播且原子广播也可实现共识。3 个前置
- 定理CAP 定理CAP theorem网络分区期间,系统不能同时保证所有请求可用与线性一致性。3 个前置
- 定理FLP 不可能性定理FLP impossibility完全异步系统中即使只允许一个进程崩溃,也不存在保证所有可容许执行终止的确定性共识协议。3 个前置
- 应用状态机复制State machine replication让多个副本按同一确定顺序执行命令,从而实现容错服务。2 个前置3 个后续