I've thought a lot about how to designed scripting and programming languages and I always run into the same problem: Control flow.
No matter how I look at it, in order to write programs, every programming language needs some way for the programmer to change the "shape" (execution path) of the algorithm. This is how the programmer imbues a program with logic to separate it from an empty state graph.
My problem is that I only know this intuitively; I have no idea how to prove it. If it's true I ought to be able to prove it, right? So how do I go about doing that? When I contemplate making a language without if/then/switch gateways am I basically asking how to do logic without logic?
>>8011762
That's the first time I've seen that image, and I actually laughed. Nice.
And yes, you do need conditionals. Without *some* way of the output depending on the input, your algorithm would produce the same result every time; even with slightly looser definitions, it wouldn't even be able to represent general functions (since no piecewise defined functions.)
To actually reach the full category of algorithms, you need both conditionals and some form of recursion/loops.
>>8011857
So it's all by definition then? The logic of the algorithm is defined as the jumps?
>>8011857
this.
if i remember correctly, look up "structured program theorem". you need some minimum of properties to be able to program.
as to prove this, ask some gauss here on board.
>>8011870
>theorem
I'm kind of going for proofs though. I don't need help understanding that programs need jumps, I just need a way to prove it. My informal approach to programming has been bothering me lately.
>>8011876
how could something like that ever be proven?
>>8011936
That's basically what I'm asking. I can only sense it intuitively, I don't know how to prove it. If it's just a matter of definitions then it's proven by virtue of the definition (as a tautology). If there's something more abstract to define before algorithms, I don't know where to start to properly formalize it.
>>8011954
>define beyond algorithms
fix
>>8011857
>That's the first time I've seen that image, and I actually laughed. Nice.
Why? I don't see why it would be funny.
The glider escapes through the window...where's the punch line?
>>8011762
I'm not a programmer, really, and I don't understand your "shape".
Can you pinpoint what this moving concepts is in terms of lambda calculus?
>>8011969
>in terms of lambda calculus
Only if you're ready to teach it to me. I'm pretty skeptical of formal notions of computation so I haven't really studied them yet. I tend to think designing a clever formalism to side-step the issue is definition fuckery and doesn't really count as a proof. Not being able to express the problem in terms of lambda calculus can only say things about lambda calculus, not the basic problem itself.
>>8011981
(Assuming the problem isn't expressible in lambda calculus. It might be, I don't know.)
>>8011982
Lambda calculus is Turing-complete; any algorithm that can be expressed in some formal framework can be expressed in Lambda calculus.
If you are not going to accept the Turing-Church thesis, why are you even bother with doing anything with computations?
Sounds like you're making the transition from programming to mathematics. Research abstract machine theory. OP pic related implies you already know about cellular automata. If not, research.
>>8012376
>any algorithm that can be expressed in some formal framework
The problem is about things that might not exist in that framework. How do you prove that the system can express "every" implementable algorithm?
>>8012390
I can accept it, I'm just wondering how it would be proven.
>>8012394
>already know about cellular automata
Yes. I understand things that boil down to a finite state machines and have an "obvious"/computable control flow, I'm just wondering if the 'jumps' are a necessary component of the logic of all algorithms.
I guess my intuitive understanding might be pretty formal already, I just don't know how to tell if what I'm asking really boils down to >>8011762
>how to do logic without logic?
or if there's a more sensible question behind it that I just don't know how to ask yet.
>>8011936
without jumps there is an upper bound on the output of programs of length k. Call this B(k).
by the Church-Turing thesis, the factorial function is computable, say with program length k_0. But then there is an integer N such that N! > B(k_0). A contradiction.
>>8012431
>I can accept it, I'm just wondering how it would be proven.
It is really in the realm of philosophy so it can't be proven per se.
>>8012459
I don't buy that. You can either create a jumpless programming language or you can't. Since it's in the realm of computability, we should be able to prove whether it's possible or not. There aren't any superpositions when dealing with computation.
>>8012455
>without jumps there is an upper bound on the output
I think I must be missing something obvious here. I can intuitively see that as true, but I'm not seeing why. It goes with my intuitions on a "logic" without jumps, but I don't know how to tell that such 'logic' doesn't actually exist. Or if it does exist I don't see how would work. Must jumpless programs necessarily halt and produce finite output? I can't just put in some special symbol that produces infinite output without computed recursion?
>>8012511
>just put in some special symbol
As in, a special symbol that doesn't violate the axioms of computation theory. It's easy enough to *imagine* a magic symbol.
>>8011762
Hey OP, check this out: http://www.nand2tetris.org/
I worked through this book in my second year of my CS degree for my computer architecture course, it's very elementary (about as elementary as you can get) and takes you from the most basic components up to a computer that can run a tetris game program.
I found it one of the most fun courses of my entire degree, and the book and course itself are available free, written and used at MIT.
To answer your question, you don't necessarily need logic in a language. This is only a condition on the model of turing machines, which operates using the logic of finite state machines.
Quantum computers, however, theoretically do not need a form of logic in their languages. If you consider a computer program as a function mapping input to output, there is no inherent need for logic, we can work simply with the mechanisms of set theory. Quantum computers allow this since their design is tied to physical laws rather than using the machine logic of classical computers.
Unfortunately I doubt any of us is going to get a chance to work on a quantum computer soon. I recommend learning the above book, it will give you some great insight into how and why classical computes work the way they do, and hopefully help you along the way to your proof.
>>8012542
The way I learned about computers seems to follow about the same trajectory as that course takes. Nice to see there are people putting actual effort into making computers not seem like black boxes of supreme mystery at every corner.
>>8012511
>I can't just put in some special symbol that produces infinite output without computed recursion?
sure but the halting problem would still be decidable since you can just check for that instruction.
>>8012511
>>8013321
to elaborate: we assume every program has one input and one output or does not terminate. adding a fixed infinite loop instruction would not allows us to output larger numbers.
to make the proof more rigourous you need to chose a formal model of computation, for example turning machines or URMs. Then you assume that the intuiative notion of computations coincide with the formal notion in the system. From this you can get a formal proof that you need jumps/recusion to be able to express all computable functions.
>>8011762
The reason you can't prove it is that there are many ways to achieve the same end.
For instance, without jumps you could have self-modifying code or you could have instructions with effectively conditional execution.
You can prove that a system is turing-complete or not, but there's not a lot you can say about the requirements of turing-completeness other than the definition.
>>8012455
>without jumps there is an upper bound on the output of programs of length k.
This:
1) assumes the instruction space has an end which necessarily results in a halt, rather than being circular,
2) assumes that the program is not self-modifying, and capable of adding instructions to its end, and
3) assumes that the computer does not have an instruction to reverse the direction of execution.
>>8011981
The lambda calculus is just a programming language like any other. Scheme is what comes closest (from the practical languages) to the untyped version from the 30's. There's nothing dubious about it.
https://en.wikipedia.org/wiki/Scheme_%28programming_language%29
>>8011762
i found verilog quite illuminating with regard to some of these problems, but it didn't get me close to proving what you want
>>8013321
Good point. I guess I forgot that formal languages can still say things about otherwise "nonsensical" things.
>>8013331
Right, thanks. Have to remember that all of this is constructed logic in the first place.
>>8013883
>effectively conditional execution
Those are called jumps.
>>8013883
>self-modifying code
I'd have to think about it more, but I think those are probably jumps too. (Per my notion of jumps.)
>>8013883
>there's not a lot you can say about the requirements of turing-completeness other than the definition
That says an awful lot on its own if you think about it.
>>8013920
>rather than being circular
Circulation would require jumps. Don't think of the program as some abstract input/output machine, think of it as a block of static source code that we can magically run somehow. In terms of the code, you have a jump at some point or it'll halt for sure.
>>8013920
>the program is not self-modifying
That's how programs are defined. If we allow code modification, we lose all formal bearing. Evolving algorithms aren't strictly computational in any real sense.
>>8013920
>direction of execution
That'd be control flow/jumps. You have to think in terms of the grammar that would actually encode these concepts or you're doing techno 'magic'. I'm coming at this from a deep design standpoint as a language designer. I can't accept magic source as relevant code unless I can actually make it magic.
>>8014001
Interesting. That tells me 90% of what I need to know. Still doesn't answer my question since my question exists one level of abstraction above any current method of algorithm expression.
>>8014032
This post: >>8013331
Answered my question most directly. I was asking how I'd go about proving it more than I was asking for a proof. I just got confused because I was thinking in terms of creating the language itself.
