Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Your conclusion is spot on.

The untyped lambda calculus is inconsistent.

If the guarantee you want from your system is consistency then you don’t want the untyped lambda calculus.

As software engineers who inherently understand system fragility as being an undesirable property we actually prefer para-consistent systems because they don’t “explode” under contradictions.

If the principle of explosion entails fragility; paraconsiatency entails anti-fragility.



An honest question - what is the problem with inconsistency in using lambda calculus as a programming language and not as foundation of mathematics?

"""The lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.[7][a] The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.[8][9]""" https://en.wikipedia.org/wiki/Lambda_calculus#History


Practically nothing.

By virtue of all programming being resource-bounded computations can be interpreted in Linear logic [1]. Linear logic is paraconsistent [2] not consistent.

Untyped Lambda calculus is essentially an assembly language and Assembly languages treat their own code as data [3]. Contradictions arrise when a system can mutate its own state. That is the power and pitfall of reflection [4]

[1] https://en.wikipedia.org/wiki/Linear_logic

[2] http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/parac...

[3] https://en.wikipedia.org/wiki/Metaprogramming

[4] https://en.wikipedia.org/wiki/Reflective_programming




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: