Talk:Structural induction

Problems (2003)

There are a few problems in this page - for example the use of the = symbol to denote equality could be problematic. Haskell would use == for this, but the intention is not to create a single Haskell expression, but rather two expressions which evaluate to the same end result. It might be better to use some other notation e.g '=' ...—Preceding unsigned comment added by 195.137.39.195 (talk • contribs) 09:39, 16 April 2003

I'm not sure I understand what you think the problem is. The "=" sign here is being used to denote numeric equality. As you say, the Haskell notation "==" would be inappropriate. If you think it would be "better" to use some nonstandard notation such as "'='", perhaps you could say why? -- Dominus 22:02, 12 May 2004 (UTC)

Problems (2004)

"The structural induction proof then consists of proving that the proposition holds for all the minimal structures, and that if it holds for the substructures of a certain structure S, then it must hold for S also."

The phrase "and that if it holds for the substructures of a certain structure S, then it must hold for S also" is too vague and lacks a definite math'l content.—Preceding unsigned comment added by 24.47.177.165 (talk • contribs) 16:02, 12 May 2004

Although this is vague, it is in the introductory paragraph. The idea is explained more formally later on. Although this may not be appropriate style for a mathematics paper, it is correct for an encyclopedia, which is aimed at a general audience. -- Dominus 22:02, 12 May 2004 (UTC)

Translation needed

There's a sentence in a foreign language (just before the formula). I'm not going to translate it, since i cannot understand that tongue. However it would be nice if someone would translate it, or (if no other option is possible) remove it.—Preceding unsigned comment added by 213.140.22.78 (talk • contribs) 22:42, 28 January 2007

General well-founded vs. structural induction?

As far as I remember, the notion of well-founded (a.k.a. noetherian) induction is more general than that of structural induction. While the former deals with arbitrary well-orderings, the latter is only about orderings of the kind "... is a part of ..." in sets of structures built-up from constructors . In fact, all examples given in the article (viz. natural numbers, lists, trees) are about constructor-term domains. I think, the article should make the distinction between well-founded and structural induction more clear. It should also mention that from any datatype declaration in (e.g.) Standard-ML , a corresponding structural induction rule can be generated mechanically.

Example:

Datatype declarations:

  datatype Nat
    = 0
    | s of Nat
  datatype Tree
    = nil
    | node of Tree * Nat * Tree

Corresponding structural induction scheme:

$P_{Nat}(0)$

$\forall n:Nat.\;P_{Nat}(n)\Rightarrow P_{Nat}(s(n))$

$P_{Tree}(nil)$

$\forall l,r:Tree,n:Nat.\;P_{Tree}(l)\land P_{Nat}(n)\land P_{Tree}(r)\Rightarrow P_{Tree}(node(l,n,r))$

------------------------------------------------------------------------------------------------------------------------------------

$\forall n:Nat.\;P_{Nat}(n)$

$\forall t:Tree.\;P_{Tree}(t)$

A well-founded indcution proof that is no structural one can be found e.g. at Unification_(computer_science)#Proof_of_termination, where the induction is along the lexicographic ordering on $Nat\times Nat\times Nat$.

Jochen Burghardt (talk) 10:57, 21 May 2013 (UTC)

Example hard to read

The example on this page requires knowledge of some sort of programming language with unexplained annotations. It attempts to teach the relevant syntax of the language, but I didn't want to spend time wrestling with this language so I went elsewhere to find a readable example that was also much shorter. Could somebody provide a shorter example that's in formal mathematical english? A good model, in my opinion, would be the page on Mathematical Induction.

I added a simpler example ("ancestor trees"). However, I feel that my explanation is still rather clumsy. Any improvements are welcome. - Jochen Burghardt (talk) 21:59, 11 October 2013 (UTC)