有限状态机:让代码成为解释窗口
用一个可验证的确定性自动机串起公式、类型语义、运行结果、交互图和审阅意见。
问题
普通代码块能说明“写了什么”,却很难同时回答三个问题:符号的类型是什么、结果是否真实运行过、图示与一般结论之间有什么边界。本文用一个只有三个状态的确定性有限自动机建立最小而完整的解释链。
直觉
输入字符串可以看作一条路径。每读一个字符,当前位置沿唯一一条边移动;读完时位于接受状态,字符串就被接受。第一段代码同样启用 Twoslash:聚焦 State、input、trace 或 formatTrace 即可读取类型。
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): stringAdds all the elements of an array separated by the specified separator string.join(' → ');
}
var console: Consoleconsole.Console.log(...data: any[]): voidThe **`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));
形式化
令状态集合为 ,字母表为 。扩展转移函数由单步转移递归定义:
因此输入 ab 的轨迹可由 式 (1) 逐步计算。下面是唯一显式启用 Twoslash 的语义场景;把焦点移到代码内的类型节点,或展开下方语义条目,即可读取定义、类型和诊断。
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 readonlyReadonly<type Record<K extends keyof any, T> = { [P in K]: T; }Construct a type with a set of properties K of type TRecord<type State = "q0" | "q1" | "q2"State, type Readonly<T> = { readonly [P in keyof T]: T[P]; }Make all properties in T readonlyReadonly<type Record<K extends keyof any, T> = { [P in K]: T; }Construct a type with a set of properties K of type TRecord<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: StateafterA;
step 的类型
(state: State, symbol: Symbol) => State
穷尽性检查
TypeScript 5.9.3 编译通过;所有 State/Symbol 组合均存在。
{"input":"ab","trace":["q0","q1","q2"],"accepted":true}
结果
固定输入 ab 的确定性检查得到轨迹 q0 → q1 → q2,最终位于接受状态。该结果来自版本固定的 TypeScript 源码和仓库内 JSON,不是语言模型计算。
有限状态轨迹
拖动步数,观察输入符号如何把当前状态沿确定性边推进。静态首帧显示第 0 步。
第 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;页面没有数学运行时。