<p>This is a repost of <a href="https://mathoverflow.net/questions/460527/when-is-an-upper-bound-on-the-longest-irreducible-program-outputting-something-c">this</a> mathoverflow question.</p>
<p>Given some way to to encode programs to strings with a finite alphabet, which we assume has a computable translation to/from Turing machines, a program is irreducible if no subsequence of it has the same behavior as it.</p>
<p>Given a string <span class="math-container">$s$</span>, we are interested in the longest irreducible program outputting it, and an upper bound on its length. Due to Higman's lemma, the set of irreducible programs outputting <span class="math-container">$s$</span> is finite, so such a bound must exist.</p>
<p>When is it computable? In particular, what happens in untyped lambda calculus? What about real world programming languages? (See <a href="https://mathoverflow.net/a/460533/498835">this answer</a> on mathoverflow for an example of an artificial encoding where it's non-computable)</p>
<p>Another question which might be simpler is to show a reduction between computing this function in different languages — I don't know how to do this even for very similar languages, like untyped lambda calculus with variable names compared to De-Bruijn indices.</p>

CC BY-SA 4.0
2024-08-11T18:13:59.530Z
Aren't prefix free code a way to code Turing machine such that no description is the prefix of another ?
ULechine
CC BY-SA 4.0
2024-08-11T18:15:01.543Z
Note that this isn't talking about prefixes — the relation here is taking a subsequence. That is, erasing some of the characters in the program
Command Master
CC BY-SA 4.0
2024-08-11T18:24:55.750Z
Is there something that makes you think it could be computable ? Because it looks a lot like a trivially uncomputable problem (when the languages are TM complete). The example of unary language is given in the math overflow question but i don't agree with OP, how do you check that the program will stop running ?
ULechine
CC BY-SA 4.0
2024-08-11T18:30:06.340Z
Why is this sequence <M>#0^n (for any n), not an infinite sequence outputting the same s ?
ULechine
CC BY-SA 4.0
2024-08-12T02:13:59.907Z
@ULechine why do you disagree with the Unary example? We can easily construct a program with the desired behavior, and any longer program with that behavior is surely not irreducible, as we can remove characters to get to our shorter program, so the length of this program must be an upper bound
Command Master
CC BY-SA 4.0
2024-08-12T02:15:01.740Z
@ULechine these aren't irreducible, because you can erase the zeros without changing the behavior of the program
Command Master
CC BY-SA 4.0
2024-08-12T13:24:11.553Z
Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/154608/discussion-between-ulechine-and-command-master).
ULechine
CC BY-SA 4.0
2024-08-16T21:45:11.657Z
I’m voting to close this question because the answer was already given at https://mathoverflow.net/questions/460527/when-is-an-upper-bound-on-the-longest-irreducible-program-outputting-something-c/460533#460533 It's not nice of you to repost the question elsewhere, when you already got an answer.
Andrej Bauer
CC BY-SA 4.0
2024-08-17T03:40:19.520Z
@AndrejBauer this isn't a complete answer, and seeing as it was 8 months ago, and I mentioned in here that it is a repost, I believe this is OK. See https://cstheory.meta.stackexchange.com/questions/1540/can-i-migrate-this-problem-from-mo-to-here for an example of a similar case.
Command Master
<lo.logic><computability><pl.programming-languages><lambda-calculus><decidability>
When is an upper bound on the longest irreducible program outputting something computable?
Command Master
# When is an upper bound on the longest irreducible program outputting something computable?

(Asked by: username_0 on 2024-08-08)

This is a repost of [this](https://mathoverflow.net/questions/460527/when-is-an-upper-bound-on-the-longest-irreducible-program-outputting-something-c) mathoverflow question.

Given some way to to encode programs to strings with a finite alphabet, which we assume has a computable translation to/from Turing machines, a program is irreducible if no subsequence of it has the same behavior as it.

Given a string $s$, we are interested in the longest irreducible program outputting it, and an upper bound on its length. Due to Higman's lemma, the set of irreducible programs outputting $s$ is finite, so such a bound must exist.

When is it computable? In particular, what happens in untyped lambda calculus? What about real world programming languages? (See [this answer](https://mathoverflow.net/a/460533/498835) on mathoverflow for an example of an artificial encoding where it's non-computable)

Another question which might be simpler is to show a reduction between computing this function in different languages — I don't know how to do this even for very similar languages, like untyped lambda calculus with variable names compared to De-Bruijn indices.

**Tags:** lo.logic, computability, pl.programming-languages, lambda-calculus, decidability
> **Comments:**
> **username_1**: Aren't prefix free code a way to code Turing machine such that no description is the prefix of another ?  
> **username_0**: Note that this isn't talking about prefixes — the relation here is taking a subsequence. That is, erasing some of the characters in the program  
> **username_1**: Is there something that makes you think it could be computable ? Because it looks a lot like a trivially uncomputable problem (when the languages are TM complete). The example of unary language is given in the math overflow question but i don't agree with OP, how do you check that the program will stop running ?  
> **username_1**: Why is this sequence <M>#0^n (for any n), not an infinite sequence outputting the same s ?  
> **username_0**: @ULechine why do you disagree with the Unary example? We can easily construct a program with the desired behavior, and any longer program with that behavior is surely not irreducible, as we can remove characters to get to our shorter program, so the length of this program must be an upper bound  
> **username_0**: @ULechine these aren't irreducible, because you can erase the zeros without changing the behavior of the program  
> **username_1**: Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/154608/discussion-between-ulechine-and-command-master).  
> **username_2**: I’m voting to close this question because the answer was already given at https://mathoverflow.net/questions/460527/when-is-an-upper-bound-on-the-longest-irreducible-program-outputting-something-c/460533#460533 It's not nice of you to repost the question elsewhere, when you already got an answer.  
> **username_0**: @AndrejBauer this isn't a complete answer, and seeing as it was 8 months ago, and I mentioned in here that it is a repost, I believe this is OK. See https://cstheory.meta.stackexchange.com/questions/1540/can-i-migrate-this-problem-from-mo-to-here for an example of a similar case.  

---

## 0 answers

