User talk:Lord Farin/Backup/Definition:Formal Language

From ProofWiki
Jump to navigation Jump to search

Definition is weird

Hm, this is not how I learnt the definition of a formal language. Currently this reads:

A formal language is a structure which contains:

The third bullet point seems to me extraneous. By my reckoning, a formal language consists of:

  • a set $S$ (the alphabet) and
  • a set of words $W \subseteq \left\{ { \left({ x_1, x_2, ..., x_n }\right) : \forall i, x_i \in S}\right\}$

As I understand it, a grammar is a way to construct a set such as $W$ and thus to define a language; what use is it to include a grammar and a set of words in the definition of a formal language? — Timwi (talk) 22:36, 18 December 2012 (UTC)

I think this is done from an algorithmic perspective. Both the words and the formal grammar can be more easily realized in a computational context than the arbitrary set $W$ you propose. It seems to explain how in general formal languages are constructed (giving a grammar of WFFs); as such I think the current page is adequate and links well to most sources on the subject (though more general than most texts bother to define things). --Lord_Farin (talk) 22:44, 18 December 2012 (UTC)

Further broadening of perspective

Ben-Ari in his work that I have started covering defines a formula to be a labelled (rooted) tree (with ordering of child nodes). Given the conceptual simplicity that results (a subformula is a subtree) and in general the appeal of graphics representing things (often much more intuitive to process, e.g. commutative diagrams) I don't see a reason to restrict to words in specifying a formal language - it could equally well be a graphical language. It's a nice generalisation that Ben-Ari provides a source for. It will also come in handy to describe (eventually) proofs as labelled trees satisfying restrictions.

Explicitly, I'd like to (wherever such is appropriate) replace instances of "word" with the more general "expression" (as Definition:Expression isn't anything meaningful atm). If we are to pursue the aim of covering all (published or otherwise verifiably practised) approaches to a concept then I think this step will be inevitable. Thoughts? --Lord_Farin (talk) 11:30, 16 February 2013 (UTC)

It's not the only such source: 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability takes a similar approach, although they start with the definition of a formal system in the conventional way and then exhibit (more or less informally) an isomorphism between such a system and a rooted tree.
In my understanding the term "expression" is narrower that "word": the latter is any arbitrary string of symbols, an expression is a well-formed word. As long as the distinction is held in mind, and that both concepts are recognised, it doesn't matter what we call them as long as we register all the variant definitions.
Also worth disambiguating between "expression" and "mathematical expression" as the latter is used informally through maths, being implicitly understood and rarely defined rigorously.
To mix metaphors horrendously, you're currently treading on the same soft ground, thin ice and booby-trapped minefield that I retreat from every time I approach this area. Each work has its own separate approach, but I have been unable to create a synthesis. But if we can find that sweet spot that merges all approaches, we'll have created something seriously worth while. --prime mover (talk) 12:31, 16 February 2013 (UTC)
You are quite correct on "expression". The next words coming to mind are "arrangement" and "collation". I'd rather not redefine "word" to include pictures. Contemplating it a bit longer, I start to like "collation" more and more. You? --Lord_Farin (talk) 13:01, 16 February 2013 (UTC)
Never heard it used outside the context of catering - but I see it's a term in computer science loosely isomorphic to "ordering".
As always. If what you're adding is supported by your text sources then go for it. --prime mover (talk) 13:54, 16 February 2013 (UTC)