11

To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted. As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up in these systems (though usually not silently, as Andrej suggests), and the fix to that bug involves some changes to existing proofs, or, more likely, of the ...


10

The reason for the ban on negative occurrences can be understood by analogy with the Knaster-Tarski theorem. This theorem says that if $L$ is a complete lattice and $f : L \to L$ is a monotone function on $L$, then the set of fixed points of $f$ is also a complete lattice. In particular, there is a least fixed point $\mu{f}$ and a greatest fixed point $\...


7

Sometimes you can solve recursive equations "by luck". I presume you want to do this in sets (as opposed to some sort of domain theory) If we unfold your definition and write down the equation directly without Haskell annotations, we get $$A \cong (A \to \emptyset) \to A.$$ Let us consider two cases: If $A$ is inhabited, i.e., it contains something, then $...


3

It's hard to add anything to Andrej's or Neel's explanations, but I'll give it a shot. I'm going to try to address the syntactic point of view, rather than try to uncover underlying semantics, because the explanation is more elementary and my give a more straightforward answer to your question. I am going to work in the simply-typed $\lambda$-calculus ...


3

You should $\alpha$-rename to avoid conflict with the variable names. That is, you should prove weakening of the form: $\Gamma \vdash (\upsilon y) P$ implies $\Gamma, x : T \vdash (\upsilon y) P$. $\alpha$-equivalence and capture-avoiding substitution is an important concept to understand in type theory: I would recommend studying this concept for the ...


1

The standard text book would be Benjamin Pierce, "Types and Programming Languages". Technically, soundness is a property of a type system. Sometimes we also say informally that a type would be (un)sound for a given term, in the sense that the underlyung type system would be (un)sound if it allowed assigning this type. Nowadays, type soundness is typically ...


Only top voted, non community-wiki answers of a minimum length are eligible