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

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: