Our Native Type Universe (NTU) has been detailed through five previous papers establishing the substrate our framework's compilation pipeline targets across multiple hardware platforms. We have found in the course of that work a deeper reach this foundation makes available: negative and fractional types as native first-class constructs. James and Sabry established these dualities in 2012; Chen and Sabry later developed their categorical interpretation in compact closed categories. These dualities have practical benefit for compute modalities in our Fidelity Framework where extant general purpose compute framings lack the substrate to host them as native constructs. We see practicality with these type forms in preserving decidability and principal types through the abelian-group algebraic pattern Kennedy's dimensional types establish. The resulting isomorphisms would admit new, concise forms of resolution within our novel lowering strategy, and we sketch a notional Clef language syntax that would admit rational dimensional exponents into our algebra. We trace the implications across several problem spaces these type forms would open to our compilation and verification disciplines: Bayesian inference where fractional types would express conditioning obligations, quantum computation (and simulations) where negative types would provide the type-level adjoint, and finally adiabatic computation where the combined discipline would express Hamiltonian deformation as a reversible constraint-propagation process. The inherent structure of our NTU together with the supporting framework appears well-suited to problem spaces that current software ecosystems do not directly address, while keeping approachable development ergonomics and mature tooling aligned with operational guarantees the framework aspires to provide.


翻译:我们的原生类型宇宙(NTU)已通过五篇先前论文得到详细阐述,这些论文奠定了框架编译流水线在多种硬件平台上所针对的基础层。在此过程中,我们发现这一基础层提供了更深层的可达性:将负类型与分类型作为原生一等构造。James与Sabry于2012年确立了这些对偶性;Chen与Sabry随后在紧闭范畴中发展了其范畴论解释。这些对偶性对我们保真度框架中的计算模态具有实际效益,而现有通用计算框架缺乏承载它们作为原生构造的基础层。我们观察到,这些类型形式通过Kennedy量纲类型所建立的阿贝尔群代数模式,在保持可判定性与主类型方面具有实用性。由此产生的同构将允许在我们新颖的下沉策略中实现简洁的新型解析形式,并勾勒出一种设想的Clef语言语法,该语法可将有理量纲指数纳入我们的代数体系。我们追溯了这些类型形式将为我们的编译与验证学科开启的多个问题空间所蕴含的影响:贝叶斯推断中,分类型可表达条件化义务;量子计算(及模拟)中,负类型可提供类型级伴随;最后在绝热计算中,这一联合学科可将哈密顿量形变表达为可逆约束传播过程。我们NTU的固有结构连同支撑框架,似乎非常适合当前软件生态未能直接解决的问题空间,同时保持了可操作的开发人体工程学,并拥有与框架旨在提供的运行保证相一致的成熟工具链。

0
下载
关闭预览

相关内容

《基于分类方法的自动人机对话》
专知会员服务
27+阅读 · 2023年7月18日
非平衡数据集 focal loss 多类分类
AI研习社
33+阅读 · 2019年4月23日
深度学习文本分类方法综述(代码)
中国人工智能学会
28+阅读 · 2018年6月16日
【AAAI专题】论文分享:以生物可塑性为核心的类脑脉冲神经网络
中国科学院自动化研究所
15+阅读 · 2018年1月23日
深度学习在文本分类中的应用
AI研习社
13+阅读 · 2018年1月7日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Arxiv
0+阅读 · 5月26日
VIP会员
最新内容
综述 | 面向大模型智能体的图结构个性化记忆
专知会员服务
0+阅读 · 今天13:56
人工智能与未来空战管理
专知会员服务
6+阅读 · 9月9日
机器的崛起:美海军陆战队组建机器人营思考
专知会员服务
9+阅读 · 9月8日
无面之战:人工智能如何重绘权力版图
专知会员服务
6+阅读 · 9月8日
相关VIP内容
《基于分类方法的自动人机对话》
专知会员服务
27+阅读 · 2023年7月18日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员