Depending on what you mean by formal definition, "broad-coverage parsers" might be want you want to look into. It's the subset of NLP research that aims to be able to take in any sentence in $language, and produce some sort of structural parse of the sentence. Such a parser is essentially a "formal theory" of the language, for some definition of formal.
Two of the more widely used parsers are the Stanford Parser and the Link Grammar Parser. Both use a hybrid of symbolic and statistical methods, starting with an underlying structural theory of grammar, and then training the specific parse decisions from a labeled data set.
The problem lies with the question 'What is the English language?'
Is it what we speak? write? what we find on the web? in what social context? Given some constraints, then perhaps yes, you could write a formal grammar and have a parser accepting this language.
Maybe my answer doesn't seem helpful, but my point is that language isn't a static, fixed and closed set.
Is it what we speak? write? what we find on the web? in what social context? Given some constraints, then perhaps yes, you could write a formal grammar and have a parser
How about defining it as what the two of us speak while having a beer in San Francisco? Is that constrained enough? If not, what constraints should be added until it becomes possble to write a parser?
Absolutely not. You might have a chance with something like Lobjan, but I doubt it. This is the heart of why statistical AI stole the show in language research.
