## Decidability of equality, and soundness of expressions involving elementary arithmetic and exponentials

Let’s have expressions that are composed of elements of $$\mathbb N$$ and a limited set of binary operations {$$+,\times,-,/$$} and functions {$$\exp, \ln$$}. The expressions are always well-formed and form finite trees, with numbers as leaf nodes and operators as internal nodes, binary operations having two child sub-expressions and the functions one. A value of such an expression is interpreted to mean some number in $$\mathbb R$$.

There are two limitations on the structure of the expressions: the divisor (the right-hand sub-expression) of $$/$$ can’t be 0 and the argument of $$\ln$$ must be positive.

I have two questions about these kind of expressions:

• Is it possible to ensure “soundness” of such an expression, in the sense that the two limitations can be checked in limited time?

• is an equality check between two such expressions decidable?

These questions seem to be connected in the sense that if you’re able to check equality of the relevant sub-expression to zero, you can decide whether a division parent expression is sound, and it doesn’t seem hard to check whether a sub-expression of $$\ln$$ is positive or negative if it’s known not to be zero.

I know that equality in $$\mathbb R$$ is generally not decidable, whereas equality in algebraic numbers is. However, I wonder how inclusion of {$$\exp, \ln$$} changes the result.

(A side note: I posted an earlier version of a question with similar intent here, but it turned out to have too little thought behind it, and had unnecessary (= not related to the meat of the question) complications with negative logarithms.)

## Decidability of equality of expressions involving exponentiation

Let’s have expressions that are finite-sized trees, with elements of $$\mathbb N$$ as leaf nodes and operators and the operations {$$+,\times,-,/$$, ^} with their usual semantics as the internal nodes, with the special note that we allow arbitrary expressions as the right-hand side of the exponentiation operation. Are the equality between such nodes (or, equivalently, comparison to zero) decidable? Is the closure under these operations a subset of algebraic numbers or not?

This question is similar to this: Decidability of Equality of Radical Expressions but with the difference that here the exponentiation operator is symmetric in the type of the base and the exponent. That means that we could have exponents such as $$3^\sqrt 2$$. It isn’t clear to me, whether allowing exponentiation with irrationals retains the algebraic closure.

This question is also similar to Computability of equality to zero for a simple language but the answers to that question focused on the transcendental properties of combinations of $$\pi$$ and $$e$$, which I consider out of scope here.

## Does the underlying computational calculus in type theories affect decidability?

I’m looking for a high-level explanation although if that isn’t possible or difficult, I’d prefer references to books/papers.

I understand that modern type theory is inspired by Curry-Howard correspondence. From the Wikipedia article on Curry-Howard correspondence:

The correspondence has been the starting point of a large spectrum of new research after its discovery, leading in particular to a new class of formal systems designed to act both as a proof system and as a typed functional programming language. … This field of research is usually referred to as modern type theory.

Looking at the various type theories proposed and under development, I have a few basic questions:

1. Most modern type theories marry a type system with lambda calculus. Are there examples where a type theory uses a computational calculus other than lambda calculus?

2. At a very high level, if every modern type theory is a bundle of a type system and a computational calculus and the computational calculus is turing-complete (like lambda calculus), does the computational calculus in any way affect the decidability of decision problems like type checking, type inference, etc.? (AFAIK modern type theories tweak the type system while keeping the associated turing-complete computational calculus intact and just tweaking the type system affects decidability of type checking, type inference, etc.)

## Cyclic shift (decidability)

Instance: Turing Machine $$M$$ given by its encoding

Question: Is there a string $$x$$ for which $$M$$ accepts all cyclic shifts of $$x$$?

Need to show that this problem is undecidable, and whether it or its complement are Turing-recognizable or not.

## Decidability of two language

Consider the following language:

• L1 = { | M is a TM, u is a word, and M accepts infinite words that contains u}
• L2 = { | M is a DFA, u is a word, and M accepts infinite words that contains u}

I am trying to figure if the above languages are Turing-recognizable or not.

I tried to do a reduction from NOT-ACCEPT both cases. suppose the reduction takes and outputs my algorithm was something like that:

1. Let M run on the word w |x| steps (x is the input of M’) 2.if M accepts w, M’ rejects x
2. if M rejects w or just stopped in some state: *if x contains u, M’ accepts *if x not contains u, M’ rejects

I am really not sure if my answers are correct, in both languages it seems to work, but its sound weird that the same reduction work both for TM and DFA.

am I missing something?

## Proving decidability and undecidablity of CFL DCFL problems [closed]

I am trying to understand how can I prove various problems of CFLs and DCFLs are undecidable or undecidable.

For context free grammars $$G, G_1, G_2$$, how can I prove following problems are undecidable:

1. Whether $$L(G)$$ is a regular language?
2. Whether $$L(G)$$ is a DCFL?
3. Whether $$L(G)^c$$ is CFL?
4. Whether $$L(G_1)\cap L(G_2)$$ is CFL?

For deterministic context free grammar $$D$$ and regular grammar $$R$$, how can I prove following problems are decidable:

1. Whether $$L(D)\subseteq L(R)$$
2. Whether $$L(D)=L(R)$$
3. Whether $$L(R)\subseteq L(D)$$

I gave following attempts:

1. I know whether $$L(G)=\Sigma^*$$ is undecidable. $$\Sigma^*$$ is regular language. So, problem 1 is undecidable.
2. Undecidability of this problem follows from undecidability of 1st problem, since set of regular languages is proper subset of set of DCFLs.
3. I am unable to come up with any logic for this.
4. Given that I know whether $$L(G_1)\cap L(G_2)=\emptyset$$ is undecidable. $$\emptyset$$ is CFL. So, problem 4 is undecidable.
5. Given that I know, $$L(G)\subset L(R)$$ is decidable, $$L(D)\subset L(R)$$ is also decidable as set of DCFLs are proper subset of set of CFLs.
6. Decidability of this problem follows from 5th problem.
7. I am unable to come up with any logic for this.

Was I correct with my attempt? Also can someone help me out for problem 3 and 7?

## reduction: L1’s decidability is unknown and L2 is undecidable

Reductions can be tricky to get the hang of, and you want to avoid “going the wrong way” with them. In which of these scenarios does L1 ≤m L2 provide useful information (and in those cases, what may we conclude)?

1. L1’s decidability is unknown and L2 is undecidable (nothing)
2. L1’s decidability is unknown and L2 is decidable (L1 is decidable)
3. L1 is undecidable and L2’s decidability is unknown (L2 is undecidable)
4. L1 is decidable and L2’s decidability is unknown (nothing)

In “L1’s decidability is unknown and L2 is undecidable” I know we can not say nothing, but I can not figure out a proof why.

## decidability and reducibility

I am a bit confused on how I can show the finiteness problem is undecidable using Rice’s Theorem.

So I’ve got something like B = { | M is a TM and L(M)- finite}. I thought I could reduce A TM (determine whether a TM accepts a given input which I already know is undecidable) to B but then I’m not sure how I would construct/ describe a new Turing Machine that decides my A?

## Decidability Turing Machine

If I have the code of a TM as $$\omega$$ with $$\Sigma=\{0,1\}$$, is it decidable that $$\omega$$ is the code of an TM?

I would say yes because there is a finite number of codes of all TMs and i can create a TM that checks if the code is $$\omega$$ or it is not.

Is this the right approach?

## Can I apply Rice’s theorem to decide decidability status of these languages?

I came across these languages:

1. A Turing machine prints a specific letter.
2. A Turing machine computes the products of two numbers

I was guessing whether I can apply Rice’s theorem to decide upon above are decidable or undecidable, something like this:

1. Not all turing machine languages have specific letter, hence the property is non trivial and hence undecidable.
2. Not all turing machine languages deal with performing product of two numbers, hence this property is non trivial and hence undecidable.

Doubt is that, Rice theorem can be applied when we are talking about languages of Turing machines, not about Turing machine behavior or characteristics themselves or anything else which is not related to “only” languages they accept. I tried to interpret given problems as if they are talking about the languages accepted by those Turing machines, so that I can apply Rice’s theorem to decide their decidability status. Am I correct with this?