I wrote a Brainfuck interpreter in (binary) Lambda Calculus [1], which was included in my 2012 IOCC submission [2]. Writing a lambda calculus interpreter in BF would be a fun challenge.
there's an isomorphism, because bf is np complete, as is simply typed lc.
simply speaking, bf can implement lc, and vice versa, which would proof the claim.
Edit: the ugly bit is that IO is always an ugly hack and potentially makes the program indetermined and thus impossible to proof a priory. but one can probably prove that they are equivalently unprovable.
Comments
Is there are relationship between the lambda calculus and Brainfuck and other few instruction set languages?
Edit: well, an easy find, https://esolangs.org/wiki/Lambda_Calculus_to_Brainfuck
I wrote a Brainfuck interpreter in (binary) Lambda Calculus [1], which was included in my 2012 IOCC submission [2]. Writing a lambda calculus interpreter in BF would be a fun challenge.
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Brain...
[2] http://www.ioccc.org/2012/tromp/hint.html
Also: https://esolangs.org/wiki/Iota
there's an isomorphism, because bf is np complete, as is simply typed lc.
simply speaking, bf can implement lc, and vice versa, which would proof the claim.
Edit: the ugly bit is that IO is always an ugly hack and potentially makes the program indetermined and thus impossible to proof a priory. but one can probably prove that they are equivalently unprovable.
Do you mean turing complete?