A computational path records the steps used to establish an equality. Topologies on computational equality witnesses can depend on the chosen generators and execution schedule, even when their algebraic and homotopical meanings agree. We study continuous presentations of finite computational paths whose declared rewrites are realized by endpoint-fixed homotopies. We compare a topology retaining the full signed trace with an observable topology recording endpoints, length, and exact path realization. Continuous finite-word interpretations that are inverse up to scoped rewriting preserve trace-sensitive quotient arrows and their final composable-pair spaces. Observable quotients behave differently. Over a point with a nonempty primitive alphabet, we classify their topology: it records length parity when all named relations preserve parity, and is otherwise indiscrete. Adjoining a conservative abbreviation can therefore turn a discrete two-element quotient into an indiscrete space, even though ordinary multiplication remains continuous. A circle presentation also gives nonhomeomorphic quotients under binary and equal-slot timing. Geometric completeness alone does not identify the trace-sensitive and observable topologies. Multiplication is continuous on the quotient of composable representatives. We characterize when this topology agrees with the ordinary pullback topology and give an open-projection criterion. Universal presentations recover classical fundamental-groupoid topology. Normal forms, primitive interchange, and a Cayley covering prove completeness for circle, torus, product, and rose presentations. A literal-word correspondence relates the semantics to the reflexivity, symmetry, and transitivity fragment of equality derivations. Selected results are formalized in Lean, with the realization models and proof coverage stated explicitly.


翻译:暂无翻译

0
下载
关闭预览

相关内容

FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
35+阅读 · 2019年10月18日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
近期语音类前沿论文
深度学习每日摘要
14+阅读 · 2019年3月17日
类脑计算的前沿论文,看我们推荐的这7篇
人工智能前沿讲习班
21+阅读 · 2019年1月7日
下载 | 866页《计算机视觉:原理,算法,应用,学习》第五版
机器学习算法与Python学习
24+阅读 · 2019年1月1日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
国家自然科学基金
9+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
12+阅读 · 2014年12月31日
国家自然科学基金
3+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
VIP会员
最新内容
《面向国防领域的大语言模型基准测试与适配》
专知会员服务
16+阅读 · 10月28日
世界模型入门:从序贯决策到通用智能体
专知会员服务
17+阅读 · 10月24日
相关VIP内容
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
35+阅读 · 2019年10月18日
相关基金
国家自然科学基金
9+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
12+阅读 · 2014年12月31日
国家自然科学基金
3+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员