探索
探索
讲义
小文章
讨论室
写作
写作
新页面
写作计划
上传文件
搜索
搜索
个人工具
创建账户
登录
通知
名字空间
模板
讨论
视图
查看
查看源代码
历史
模板: 类型论
根据香蕉空间的设计目标, 类型论板块尽可能只关注现代类型论, Russell 那一套东西、计算机相关 (比如面向对象类型系统) 就不要划在类型论板块里了.
待完善词条:
Martin-Löf 类型论
同伦类型论
概括范畴
立方类型论
N-类型
参数性
具现
类型论
基本概念
类型
•
语境
•
替换操作
•
λ
编码
•
Curry–Howard 对应
•
模式匹配
一般类型论
简单类型
λ
演算
•
函数
、
积
、
无交并
•
归纳类型
、
余归纳类型
(
互拟
)
•
自然数
•
纯类型论
、
F 系统
•
子类型
依值类型论
Martin-Löf 类型论
•
宇宙
、
命题宇宙
、
集合
•
相等类型
•
W
类型
、
M
类型
•
观测类型论
•
构造演算
同伦类型论
圆周
、
区间
、
纬悬
•
逻辑截断
、
截断
•
n
-类型
•
高阶归纳类型
•
立方类型论
•
高阶观测类型论
类型论性质
正规性
、
典范性
•
Tait 可计算性
•
一致性
•
参数性
•
合流性
•
非直谓性
•
类型不变性
语义与模型
范畴语义
、
概括范畴
、
C 系统
•
语汇理论
•
偏等关系语义
•
具现
[
查看模板
]