Jump to content

Talk:Structural induction

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

Problems (2003)

[edit]

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 (talkcontribs) 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)[reply]

Problems (2004)

[edit]

"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 (talkcontribs) 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)[reply]

Translation needed

[edit]

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 (talkcontribs) 22:42, 28 January 2007

General well-founded vs. structural induction?

[edit]

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 [1]. 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 [2], 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:

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

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 .

  1. ^ This view is supported by this article Noetherian_induction#Induction_and_recursion which says "When the well-founded set is a set of recursively-defined data structures, the technique [of well founded induction] is called structural induction."
  2. ^ similar for each particular initial algebra

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

Example hard to read

[edit]

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)[reply]