“Propositions as Types“ by Philip Wadler 听不懂的学习笔记
“Propositions as Types“ by Philip Wadler 听不懂的学习笔记
本文搬运自本人高中时期CSDN博客，若图片加载不出来，可到原文查看：https://blog.csdn.net/zhangtingxiqwq/article/details/162107745
- David Hilbert
put maths to alogo
provable statement
- Kurt
statement it nt provble
you prove sth is false
it 's true but no provable
formal definiton
- Alonzo Church
lambda calculus
halting proble
- Kurt
second definition
the same as you
- Alan Turing
Turing Machine
als equal
computer = turing machine
all three same
mathematic invented or discovered?
you discover!
Part II Propositions as types
- Gerhard Gentzen
Natural Deducion
implication
elimination rules
A proof
know A and B, i can know B and A
a formal proof
simplifying proofs
sub formular
formulars ->
proof can be simpled
听不懂，放弃了
本博客所有文章除特别声明外，均采用 CC BY-NC-SA 4.0 许可协议。转载请注明来源 zhangxixi的博客！
相关推荐
2026-06-28
《具体数学》Lesson 1：Recurrent Problem学习笔记
《具体数学》Lesson 1：Recurrent Problem学习笔记 本文搬运自本人高中时期CSDN博客，若图片加载不出来，可到原文查看：https://blog.csdn.net/zhangtingxiqwq/article/details/162397627 Recurrent Problem 递归问题 Mathematical Induction 数学归纳法 Every recurrence problem can be divided into 3 parts : (1) Research on the small situations (2) Give the rec...
2026-06-19
线性代数学习笔记（第 6- 10 课）
线性代数学习笔记（第 6- 10 课） 本文搬运自本人高中时期CSDN博客，若图片加载不出来，可到原文查看：https://blog.csdn.net/zhangtingxiqwq/article/details/162126613 线性代数学习笔记（6-10课） 第六课：分块矩阵 I 分块运算的规则 分块矩阵 运算规则 加法 乘法 前提： AAA 的列分发和 BBB 的行分法必须完全相同 II 分块对角阵的性质 定义：一个分块矩阵除了主对角线上的子块外，其余所有子块都是零矩阵 形式： 性质： 行列式等于对角块行列式之积 逆矩阵等于对角块逆矩阵的分...
2026-06-19
线性代数学习笔记（第 1 - 5 课）
线性代数学习笔记（第 1 - 5 课） 本文搬运自本人高中时期CSDN博客，若图片加载不出来，可到原文查看：https://blog.csdn.net/zhangtingxiqwq/article/details/162118601 线性代数学习笔记（1-5） 第一课：矩阵运算体系 I 矩阵线性运算 同型矩阵：即行数相同、列数也相同的矩阵 矩阵加 A+B=[a11+b11a12+b12a21+b21a22+b22]A + B = \begin{bmatrix} a_{11}+b_{11} & a_{12}+b_{12} \\ a_{21}+b_{21} & a...
2026-05-23
Git基础命令学习笔记
Git基础命令学习笔记 本文搬运自本人高中时期CSDN博客，若图片加载不出来，可到原文查看：https://blog.csdn.net/zhangtingxiqwq/article/details/161336335 你现在在你的文件夹内打开cmd 开始 1git init 修改 12git add . git commit -m "version1" 在本地随便commit都没有任何问题，不会上传到github，方面本地备份代码。 上传github 先在github上建一个仓库 第一次推送 12git remote add origin 仓库地址gi...
2023-09-16
FWT笔记存档
FWT笔记存档 本文搬运自本人高中时期CSDN博客，若图片加载不出来，可到原文查看：https://blog.csdn.net/zhangtingxiqwq/article/details/132922560
2023-12-29
12.29听课笔记
12.29听课笔记 本文搬运自本人高中时期CSDN博客，若图片加载不出来，可到原文查看：https://blog.csdn.net/zhangtingxiqwq/article/details/135297427 A 1，n个0，n个1 B -1 放最小 +1 放最大 C 假如根定，可以直接dp 打表得只要根是叶子，答案取最小 直接暴摊也是对的 D 假如定根， DPuDP_uDPu 内部分辨要多少个点。则 DPu=∑DPv−[存在一个儿子为叶子且分支>1]DP_u=\sum DP_v-[存在一个儿子为叶子且分支>1]DPu=∑DPv−[存在一个儿子为叶子且分支&...