Impredicative images

Three images, spotted by Ohad Kammar (@aleph_kappa). Ohad suggests they illustrate recursion, but I think they represent impredicativity. Impredicativity is a category error, when a predicate applies to itself, as in Russell's paradox; but also a defining feature of polymorphic lambda calculus, where a function abstracted over a type may be applied to its own type.

Labels: ,

Thanks for suggesting impredicativity instead --- it's much more suitable. :)

Two comments:

1. I disagree that impredicativity is a 'category error'. Impredicativity is 'safe' if the entity being defined can also be defined by some other means. Universal properties and the proof for Goedel's Incompleteness Theorem are safe instances of impredicativity.

Whether having impredicative syntax is safe or not, such as the polymorphic lambda calculus, is a matter of taste ;).

2. Less seriously, the post's title is incorrect: these images are not impredicative, they only depict impredicativity. :)
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?