1
$\begingroup$

There are a ton of resources on the web devoted to proving some esoteric language is Turing complete by simulating arbitrary turing machines. I have an esoteric language I want to prove is complete, but I'm pretty sure the easier way to do it would be to prove that you can express any untyped lambda calculus term in it; i.e.

Recursively, it can represent a name, x. Given a lambda term E1 and E2 and a name v, it can represent lambda v.E1 as well as (E1)(E2).

Are there any existing examples of trying to prove a language is Turing complete through reduction to untyped (or any other Turing-complete) lambda calculus rather than through reduction to whether a Turing Machine halts?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

Yes, I think the most famous example is the $\pi$-calculus, which Milner showed to be complete by such a reduction in Functions as Processes.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Here's another one, which encodes combinatory logic into Featherweight Java. $\endgroup$
    – cody
    Commented May 23, 2023 at 21:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.