COMP4161 Isabelle 代写
## COMP4161 T3/2024软件验证高级主题作业1
本作业于2024年9月19日星期四开始，截止日期为2024年9月26日星期四23:59:59。我们接受纯文本（.txt）文件、PDF（.pdf）文件和Isabelle理论（.thy）文件。你可以在截止日期后最多五天（120小时）内迟交，但会有扣分：每天扣5分。本作业为带回家完成的作业。这并不意味着你可以小组合作。每份提交都是个人的。更多信息，请参阅抄袭政策：https://student.unsw.edu.au/plagiarism。你不允许使用AI工具（如ChatGPT或GitHub Copilot）来帮助你处理技术内容，或开发定义和证明。在CSE机器上使用give提交：
give cs4161 a1 files…
give cs4161 a1 a1.thy a1.pdf
## 1. λ-演算（16分）
通过应用语法约定和规则，对项\((pq)(\lambda p\cdot(\lambda q\cdot(\lambda r\cdot(q(rp))))))\)进行语法简化。证明你的答案。（2分）
恢复项\(a(\lambda ab.(bc)a(bc))(\lambda b.cb)\)中省略的括号（但确保不改变项结构）。（2分）
求\((\lambda f\cdot\lambda x\cdot f(fx))(\lambda g\cdot\lambda y\cdot g(g(gy)))\)的范式。通过展示归约序列来证明你的答案。归约序列中的每一步应该是一个单一的β-归约步骤。为每一步下划线或用其他方式指示被归约的项（redex）。（6分）
回忆讲座中看到的λ演算中自然数的编码（丘奇数）：
\(0\equiv\lambda fx,x\)
\(1\equiv\lambda fx.fx\)
\(2\equiv\lambda fx.f(fx)\)
\(3\equiv\lambda fx.f(f(fx))\cdots\)
定义\(exp\)，其中\(exp\ m\ n\)β-归约到表示\(m^n\)的丘奇数。证明你的答案。（6分）
## 2. 类型（20分）
为项\(\lambda abc.a(xbb)(cb)\)提供最一般类型。展示类型推导树来证明你的答案。树的每个节点应该对应于单个类型规则的应用，并标有所用的类型规则。该项在哪些上下文中类型正确？（5分）
找到一个具有以下类型的闭λ项：
\((‘a\Rightarrow’b)\Rightarrow(‘c\Rightarrow’a)\Rightarrow’c\Rightarrow’b\)
（你不需要提供类型推导，只需要提供项）。（4分）
解释为什么\(\lambda x.xx\)不可类型化。（3分）
求\((\lambda fx.f(xx))(\lambda yz.z)\)的范式及其类型。（3分）
\((\lambda fx.f(xx))(\lambda yz.z)\)是否可类型化？将这种情况与你在讲座中学到的主体归约进行比较。（5分）
## 3. 命题逻辑（29分）
仅使用以下证明方法：rule、erule、assumption、cases、frule、drule、rule tac、erule tac、frule tac、drule tac、rename tac和case tac；以及仅使用以下证明规则：impI、impE、conjI、conjE、disjI1、disjI2、disjE、notI、notE、iffI、iffE、iffD1、iffD2、ccontr、classical、FalseE、TrueI、conjunct1、conjunct2和mp，证明以下每个陈述。你不需要使用所有这些方法和规则。
\(x\to\neg\neg x\)（3分）
\((X\to Y\to\neg X)\to X\to\neg Y\)（3分）
\(\neg\neg A\to A\)（4分）
\(\neg(A\land B)\to\neg A\vee\neg B\)（4分）
\(\neg(A\to B)\to A\)（4分）
\((\neg A\land\neg B)=(\neg(A\vee B))\)（6分）
\((A\to B)\to((B\to C)\to A)\to B\)（5分）
## 4. 高阶逻辑（35分）
仅使用上一个问题中提到的证明方法和证明规则，以及以下任何证明规则：allI、allE、exI和exE，证明以下每个陈述。你不需要使用所有这些方法和规则。在证明后面的部分时，你可以使用在前面部分证明的规则。
\((\forall x.\neg Px)=(\nexists x.Px)\)（4分）
\((\exists xy.Pxy)=(\exists yx.Pxy)\)（4分）
\((\exists x.Px\to Q)=((\forall x.Px)\to Q)\)（7分）
\(((∀x.Px)→(∃x.Qx))=(∃x.Px→Qx)\)（7分）
\(\forall x.\neg Rx\to R(Mx)\Rightarrow\forall x.Rx\vee R(Mx)\)（6分）
\([\forall x.\neg Rx\to R(Mx);\exists x.Rx]\Rightarrow\exists x.Rx\land R(M(Mx))\)（7分）