LEAN 类型系统属性 之 算法式相等的非传递性(Algorithm equality is not transitive)注解

news2024/11/8 1:47:07

        由于 subsingleton 使用函数(eliminator) 的存在,导致算法式相等(Algorithm defintional equality)的非传递性。

在《定义上相等的非确定性(Undecidability of Definitional Equality)》 中有,

其中,定义上相等可替换规则起来作用:

同时,根据 归纳类型(Inductive Type)的简化规则(Reduction Rule),有:

简单来看是,intro 0 inv 0 a 的类型为 acc 0,而 inv 0 a 1 (p 0) 的类型为 acc 1,即两者的类型不同。由此,

实际上是,可达类型(Accessibility Type)中,

其使用规则定义的使用函数,是 subsingleton 使用函数(eliminator):

        这里,由于可达类型(Accessibility Type)的 subsingleton 使用函数(eliminator)在使用前值、前果时,由于前值与现值不属于同一类型,即 acc n 和 acc (n+1),因此,有,

        但是,f 0 a 没有使用规则(Elimination Rule)用于产生 f 1 (inv 0 a 1 ( p 0 ) ),也没有已经定义的简化规则可以使用,因此,

        在LEAN的设计上,算法式定义上相等是可确定的(Decidable),而定义上相等是不确定的(undecidable),由此,有些定义上相等的推演规则是没有对应的算法式定义上相等的规则,如 传递性(transitivity)只存在于定义上相等,也导致了其不确定性,即在判断定义上相等时,会陷入不能停止(non-terminated)。

        这里需要明确的是,LEAN系统内的所有能使用的转化规则,赋型规则等,都必须是LEAN显示(Explicit)定义的。

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.coloradmin.cn/o/2130123.html

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈,一经查实,立即删除!

相关文章

[基于 Vue CLI 5 + Vue 3 + Ant Design Vue 4 搭建项目] 10 Ant Design Vue 的注册

1.全局全部注册 这样就可以将 ant design vue 全部组件注册进来 2.全局部分注册 这样就是按需注册了 本次, 我们选择第1种方式,全部注册进来 3.注册全局 css 4.测试一下 在 AboutView.vue 中添加一个 Test 按钮 使用 npm run serve 启动服务 访问 A…

如何通过subprocess在数据采集中执行外部命令 —以微博为例

介绍 在现代网络爬虫开发中,爬虫程序常常需要与外部工具或命令交互,以完成一些特定任务。subprocess 是 Python 提供的强大模块,用于启动和管理外部进程,广泛应用于爬虫技术中。本文将探讨如何通过 subprocess 在爬虫中执行外部命…

k8s 常见问题梳理

1、“cni0” already has an IP address different from 10.244.2.1/24 删除网卡 ifconfig cni0 down ip link delete cni0ip link add cni0 type bridge ip link set dev cni0 up ifconfig cni0 10.244.2.1/24 ifconfig cni0 mtu 1450 up

二.Unity中使用虚拟摇杆来控制角色移动

上一篇中我们完成了不借助第三方插件实现手游的虚拟摇杆,现在借助这个虚拟摇杆来实现控制角色的移动。 虚拟摇杆实际上就给角色输出方向,类似于键盘的WSAD,也是一个二维坐标,也就是(-1,1)的范围,将摇杆的方向进行归一化…

Windows与Linux下 SDL2的第一个窗口程序

Windows效果和Linux效果如下&#xff1a; 下面是代码&#xff1a; #include <stdio.h> #include "SDL.h"int main(int argc, char* argv[]) { // 初始化SDL视频子系统if (SDL_Init(SDL_INIT_VIDEO) ! 0){// 如果初始化失败&#xff0c;打印错误信息printf(&…

HPA自动扩缩容和命名空间资源限制

目录 HPA概念 安装HPA的依赖环境 安装metrics-server 手动扩缩容 自动扩缩容 yaml文件 创建HPA 自动扩容 自动缩容 命名空间资源限制 HPA概念 HPA是针对pod的数量进行自动扩缩容。&#xff08;是针对控制器deployment、replicaset、StatefulSet创建的pod&#xff0…

TS接口、泛型、自定义类型

这里记录下typescript中接口、泛型和自定义类型的使用 接口定义 // 定义一个接口,用来限制Teacher的属性 export interface Teacher {name: string;age: number;gender: string; }export type teacherList Teacher[];// 一个自定义类型 export type Teachers Array<Teach…

【UE5 C++课程系列笔记】02——创建C++类的三种方式

目录 一、从UE编辑器中创建 引用头文件报错的两种解决方式 &#xff08;1&#xff09;方式1 &#xff08;2&#xff09;方式2 二、在文件夹中直接创建 三、在Visual Studio中创建 一、从UE编辑器中创建 在UE编辑器中选择“Tools-》New C Class” 这里新建的类的父类选择…

Gitlab 中几种不同的认证机制(Access Tokens,SSH Keys,Deploy Tokens,Deploy Keys)

前言 公司主要使用 Go 语言做项目&#xff0c;有一些 Gitlab 私有仓库需要引用&#xff0c;在做 CI 时&#xff0c;要自行配置权限以获取代码。 最近发现各个项目组在做 CI 遇到仓库权限问题时的解决方式不尽相同&#xff0c;有用 Project Token 的&#xff0c;有用 Deploy K…

【python】OpenCV—Augmented Reality Using Aruco Markers

文章目录 1、任务描述2、Aruco Markers3、代码实现4、更多例子展示5、涉及到的库cv2.findHomography 6、参考 1、任务描述 借助 Aruco Markers&#xff0c;替换墙面上画面中的内容 2、Aruco Markers OpenCV 中的 aruco 模块共有 25 个预定义的标记字典。字典中的所有标记包含…

新代机床采集数据

新代集團1995年成立於台灣新竹,事業版圖遍布全球,以台灣為中心向外發展,據點橫跨歐洲、美洲、亞洲三大洲。新代長期深耕於機床控制器的軟體及硬體技術研發,專注於運動控制領域,目前已成為亞太市場中深具影響力的控制器領導品牌之一。主營產品包括:機床數控系統、伺服驅動…

Java虚拟机 - 高级篇

一、GraalVM 1. 什么是GraalVM 2. GraalVM的两种运行模式 &#xff08;1&#xff09;JIT即时编译模式 &#xff08;2&#xff09;AOT提前编译模式 3. 应用场景 4. 参数优化和故障诊断 二、新一代的GC 1. 垃圾回收器的技术演进 2. Shenandoah GC 测试代码&#xff1a; /** C…

Ubuntu 20.04/22.04无法连接网络(网络图标丢失、找不到网卡)的解决方案

问题复述&#xff1a; Ubuntu 20.04无法连接到网络&#xff0c;网络连接图标丢失&#xff0c;网络设置中无网络设置选项。 解决方案 对于Ubuntu 20.04而言&#xff1a;逐条执行 sudo service network-manager stopsudo rm /var/lib/NetworkManager/NetworkManager.statesudo…

《深度学习》OpenCV轮廓检测 模版匹配 解析及实现

目录 一、模型匹配 1、什么是模型匹配 2、步骤 1&#xff09;提取模型的特征 2&#xff09;在图像中查找特征点 3&#xff09;进行特征匹配 4&#xff09;模型匹配 3、参数及用法 1、用法 2、参数 1&#xff09;image&#xff1a;待搜索对象 2&#xff09;templ&am…

利用AI驱动智能BI数据可视化-深度评测Amazon Quicksight(四)

简介 随着生成式人工智能的兴起&#xff0c;传统的 BI 报表功能已经无法满足用户对于自动化和智能化的需求&#xff0c;今天我们将介绍亚马逊云科技平台上的AI驱动数据可视化神器 – Quicksight&#xff0c;利用生成式AI的能力来加速业务决策&#xff0c;从而提高业务生产力。…

科技之光,照亮未来之路“2024南京国际人工智能展会”

全球科技产业的版图正以前所未有的速度重构&#xff0c;而位于中国东部沿海经济带的江浙沪地区&#xff0c;作为科技创新与产业升级的高地&#xff0c;始终站在这一浪潮的最前沿。2024年&#xff0c;这一区域的科技盛宴——“2024南京人工智能展会”即将在南京国际博览中心盛大…

基础的八股

JS this 全局&#xff1a;this指向window 函数&#xff1a;this指向window 对象&#xff1a;this指向调用它的 get、post的区别 1、写的地方不同&#xff1a;get在地址栏里 地址栏有多长就只能写多少、post在请求体里 没有上限 2、关于回退和刷新&#xff1a;get回退和刷新没问…

TCP、UDP、HTTPS、HTTP

前言 OSI七层网络 名称解释协议应用层定义了各种应用协议的数据规范 HTTP、HTTPS、SSL FTP、DNS TFTP、SMTP 表示层不同系统之间通信会话层断点续传传输层 一个电脑有许多端口&#xff0c;根据端口找到发送方与接收方 确保数据包完整性 TCP、UDP网络层 ARP协议&#xff1a;通过…

shopify主题布局layout

一、基本概念 Layout是Shopify主题中的基础结构&#xff0c;它决定了页面的整体框架和布局方式。通过Layout&#xff0c;可以统一管理和控制页面上的公共元素&#xff0c;如页眉&#xff08;Header&#xff09;、页脚&#xff08;Footer&#xff09;等&#xff0c;确保这些元素…

闯关leetcode——20. Valid Parentheses

大纲 题目地址内容 解题代码地址 题目 地址 https://leetcode.com/problems/valid-parentheses/description/ 内容 Given a string s containing just the characters ‘(’, ‘)’, ‘{’, ‘}’, ‘[’ and ‘]’, determine if the input string is valid. An input st…