How do I prove that smth is undecidable

@haskal uhhhhh something along the lines of "given this fixed set of derivation rules and these two terms, is there a derivation showing that they are convertible"

@ionchy @haskal Is there known theorem about undecidability of convertibility of a known language? Then maybe you can encode that language in yours in a clever way

@turion hmm... maybe
I'd expect some sort of extensional language with reflection to have undecidable conversion...

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.