verified note

有限状态机:让代码成为解释窗口

用一个可验证的确定性自动机串起公式、类型语义、运行结果、交互图和审阅意见。

问题

普通代码块能说明“写了什么”,却很难同时回答三个问题:符号的类型是什么、结果是否真实运行过、图示与一般结论之间有什么边界。本文用一个只有三个状态的确定性有限自动机建立最小而完整的解释链。

直觉

输入字符串可以看作一条路径。每读一个字符,当前位置沿唯一一条边移动;读完时位于接受状态,字符串就被接受。第一段代码同样启用 Twoslash:聚焦 StateinputtraceformatTrace 即可读取类型。

trace.tsTwoslash · build time
type type State = "q0" | "q1" | "q2"State = 'q0' | 'q1' | 'q2';

const const input: readonly ["a", "b"]input = ['a', 'b'] as type const = readonly ["a", "b"]const;
const const trace: readonly State[]trace: readonly type State = "q0" | "q1" | "q2"State[] = ['q0', 'q1', 'q2'];

function function formatTrace(states: readonly State[]): stringformatTrace(states: readonly State[]states: readonly type State = "q0" | "q1" | "q2"State[]) {
  return states: readonly State[]states.ReadonlyArray<State>.join(separator?: string): string
Adds all the elements of an array separated by the specified separator string.
@paramseparator A string used to separate one element of an array from the next in the resulting String. If omitted, the array elements are separated with a comma.
join
('');
} var console: Consoleconsole.Console.log(...data: any[]): void
The **`console.log()`** static method outputs a message to the console. [MDN Reference](https://developer.mozilla.org/docs/Web/API/console/log_static)
log
(const input: readonly ["a", "b"]input, function formatTrace(states: readonly State[]): stringformatTrace(const trace: readonly State[]trace));

形式化

令状态集合为 Q={q0,q1,q2}Q=\{q_0,q_1,q_2\},字母表为 Σ={a,b}\Sigma=\{a,b\}。扩展转移函数由单步转移递归定义:

δ^(q,ε)=q,δ^(q,wa)=δ(δ^(q,w),a).\hat\delta(q,\varepsilon)=q,\qquad \hat\delta(q,wa)=\delta(\hat\delta(q,w),a).
(1)

因此输入 ab 的轨迹可由 式 (1) 逐步计算。下面是唯一显式启用 Twoslash 的语义场景;把焦点移到代码内的类型节点,或展开下方语义条目,即可读取定义、类型和诊断。

transition.tsTwoslash · build time
export type type State = "q0" | "q1" | "q2"State = 'q0' | 'q1' | 'q2';
export type type Symbol = "a" | "b"Symbol = 'a' | 'b';
export type 
type TransitionTable = {
    readonly q0: Readonly<Record<Symbol, State>>;
    readonly q1: Readonly<Record<Symbol, State>>;
    readonly q2: Readonly<Record<Symbol, State>>;
}
TransitionTable
= type Readonly<T> = { readonly [P in keyof T]: T[P]; }
Make all properties in T readonly
Readonly
<type Record<K extends keyof any, T> = { [P in K]: T; }
Construct a type with a set of properties K of type T
Record
<type State = "q0" | "q1" | "q2"State, type Readonly<T> = { readonly [P in keyof T]: T[P]; }
Make all properties in T readonly
Readonly
<type Record<K extends keyof any, T> = { [P in K]: T; }
Construct a type with a set of properties K of type T
Record
<type Symbol = "a" | "b"Symbol, type State = "q0" | "q1" | "q2"State>>>>;
export const const transitions: Readonly<Record<State, Readonly<Record<Symbol, State>>>>transitions:
type TransitionTable = {
    readonly q0: Readonly<Record<Symbol, State>>;
    readonly q1: Readonly<Record<Symbol, State>>;
    readonly q2: Readonly<Record<Symbol, State>>;
}
TransitionTable
= {
q0: Readonly<Record<Symbol, State>>q0: { a: Statea: 'q1', b: Stateb: 'q0' }, q1: Readonly<Record<Symbol, State>>q1: { a: Statea: 'q1', b: Stateb: 'q2' }, q2: Readonly<Record<Symbol, State>>q2: { a: Statea: 'q2', b: Stateb: 'q2' }, }; export function function step(state: State, symbol: Symbol): Statestep(state: Statestate: type State = "q0" | "q1" | "q2"State, symbol: Symbolsymbol: type Symbol = "a" | "b"Symbol): type State = "q0" | "q1" | "q2"State { return const transitions: Readonly<Record<State, Readonly<Record<Symbol, State>>>>transitions[state: Statestate][symbol: Symbolsymbol]; } export const const afterA: StateafterA = function step(state: State, symbol: Symbol): Statestep('q0', 'a');
const afterA: State
afterA
;
transition-step编译器验证
TransitionTable

从状态和输入符号到下一状态的只读映射。

查看定义
step 的类型

(state: State, symbol: Symbol) => State

穷尽性检查

TypeScript 5.9.3 编译通过;所有 State/Symbol 组合均存在。

固定输入 ab 的运行结果
                  {"input":"ab","trace":["q0","q1","q2"],"accepted":true}
                
TypeScript 5.9.3 / Twoslash 0.3.98380d1d028b88380d1d028b8

结果

固定输入 ab 的确定性检查得到轨迹 q0 → q1 → q2,最终位于接受状态。该结果来自版本固定的 TypeScript 源码和仓库内 JSON,不是语言模型计算。

有限状态轨迹

拖动步数,观察输入符号如何把当前状态沿确定性边推进。静态首帧显示第 0 步。

三个状态之间的确定性转移q0 经过 a 到 q1,q1 经过 b 到 q2;当前状态随步数高亮。abq0q1q2

第 0 步:初始状态 q0。

限制

这个三状态例子只演示解释界面与确定性查表,不证明一般自动机算法的复杂度结论;SVG 中的布局也是说明性示意,不是实验数据。浏览器不会执行 TypeScript、Lean 或 Wolfram,所有语义和结果都在构建前生成。

来源

  • 源码:artifacts/semantic-window/transition.ts,由内容元数据中的不可变 SHA-256 引用。
  • 类型信息:TypeScript 5.9.3 与 Twoslash 0.3.9 在构建期生成。
  • 运行结果:transition-output.json,由仓库测试逐项核对。
  • 公式:KaTeX 在构建期输出可访问 MathML;页面没有数学运行时。