theory salon

« first day (2895 days earlier) ← previous day next day → last day (734 days later) »

Thomas Klimpel

06:41

@ConGovDeIn OK, I think I know how the "official proof" is supposed to look like. The induction should not go over the natural number, but over the tree structure of the terms. So the induction start are the leaves, i.e. the variables and constants, and the induction step is over the inner nodes, i.e. the function symbols with arity > 0.

1 hour later…

ConGovDeIn

07:45

@ThomasKlimpel can you please elaborate on “induction step is over the inner nodes” ?

Thomas Klimpel

A tree has two types of nodes: leaves and inner nodes.

ConGovDeIn

Okay.

So, leaves are the variables and constants?

And inner nodes are constructed out of leaves?

Thomas Klimpel

Induction over a tree: A proposition on a tree is true, if it is true at the leaves, and if the truth at every inner node follows from the truth of the proposition at the child nodes of the inner node.

ConGovDeIn

Oh! I shall need to study tree logic and then everything will be quite clear, I reckon.

Thomas Klimpel

no, no, that is not my point

My point was that the proof is supposed to be simple, and even my simple proof still contained that "stack", which is most probaly not part of the official proof. And the reason is that the induction in the official proof does not go over the natural numbers, but over a tree.

And proving that induction over a tree can be reduced to induction over the natural numbers is not part of the proof, you can just use the fact that induction over a tree works as "expected" (i.e. as I explained in the comment that starts with "Induction over a tree: ..."

ConGovDeIn

07:57

@ThomasKlimpel Please, it’s a request can you please once again give a formal proof using that “stack”, “pop” and “push” method? I really liked and understood it. Can you please formalise it?

Thomas Klimpel

The recursive term structure can be uniquely reconstructed from its string of symbol. One way to do this is by reading the string backward from the end to the start symbol by symbol, and manipulate a stack of terms in each step. We start with an empty stack. The desired state after reading the entire string is a stack with just a single term on it.

ConGovDeIn

Okay

Thomas Klimpel

08:19

If we read a variable or constant, then we push it on the stack. If we read a function symbol for a function of arity k, then we pop k terms from the stack, form the new term using the function symbol, and push it on the stack again.
Since the whole procedure was deterministic, it is pretty obvious that the string of symbols uniquely determines the resulting terms. For if not, suppose that we perform the procedure two times, and would end up with a differnt stack as results. Initially, both procedures start with an empty stack, so both stacks are identically initially. The induction hypothe…

For the case where a function symbol is read, the arity of the function symbol uniquely determines the number k of terms that get popped from the stack. Then the new term is formed, which might be an unclear point, since we didn't specify in detail how such a term would be represented. One way would be to represent it again as a string, but maybe this time adding brackets and commas to make the structure of the list of subterms more obvious.

ConGovDeIn

@ThomasKlimpel We can represent that “new term” which is formed from a function by, say, capital letter T?

But the explanation is quite awesome. I will go with this one. Thanks.

Thomas Klimpel

Another possibility would be to represent the new term as a tree, where a node represents a function symbol, and its children represent the subterms. But those details are not important. The new term that gets pushed on the stack is unique in a certain suitable sense, and that is all that matters.

ConGovDeIn

Yes.

Thomas Klimpel

@ConGovDeIn Well, the representation should still uniquely represent the new term, so merely pushing a capital letter T on the stack is not good enough, in a certain sense.

ConGovDeIn

08:42

Okay. But at least we have got the main idea.

Thanks for explaining that. I will be back.

« first day (2895 days earlier) ← previous day next day → last day (734 days later) »

all rooms