Mathematics and Computation

A blog about mathematics for computers

On the Failure of Fixed-point Theorems for Chain-complete Lattices in the Effective Topos

Abstract: In the effective topos there exists a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. Consequently, the Bourbaki-Witt theorem and Tarski’s fixed-point theorem for chain-complete lattices do not have constructive (topos-valid) proofs.

Download: fixed-points.pdf

Published in: Theoretical Computer Science Volume 430, 27 April 2012, Pages 43–50. Mathematical Foundations of Programming Semantics (MFPS XXV)

Comments

p.l.lumsdaine

Very nice paper!

I think there may be a typo in the first paragraph of Sect. 2, by the way: you define that X is discrete if the diagonal map X --> X^{\nabla 2} is constant. But if internally this is the condition that every map fron \nabla 2 to X is constant, i.e. in the image of the diagonal map, should the original condition be that the diagonal map is epimorphic?

Thank you for spotting that one. It should say that the diagonal map is an isomorphism, or equivalently epimorphism, as you suggest.

Post a comment:
Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.

Name

E-mail

Website

Comment