<p>Let G be a grammar that contains no left-recursive rules, and we use a recursive-descent recognizer that uses full backtracking, using list of results for example, to recognize strings of G.  </p>

<p>How can someone show formally that if s is a sentence in G, then R(G), which is the
recognizer I just described for G, can recognize s, and it also explores all the paths, i.e., if there are two paths to recognition, both can be explored.</p>

CC BY-SA 3.0
2014-09-09T22:07:09.897Z
Why do you want to do that rather than use dynamic programming which is more efficient, quadratic (for recognition only) rather than exponential, and can accept recursive rules? Also exploring all paths is useless for a recognizer: what is recognized is recognized.
babou
CC BY-SA 3.0
2014-09-09T22:12:06.510Z
My question here is not from a practicality point of view. You are right and there are indeed better options out there. I just would like to know how someone writes such proofs? How to show the correctness of a recursive-descent parser.
Wickoo
CC BY-SA 3.0
2014-09-09T22:37:46.843Z
Not much time for it just now. Can you get inpiration from what is
done to prove non-deterministic PDA recognize CF languages. After all,
your backtrack  recursive-descent is just mimicking a
non-deterministic PDA computation.
babou
<proofs><parsing><correctness>
Correctness proof of recursive-descent recognizer
Wickoo
# Correctness proof of recursive-descent recognizer

(Asked by: username_0 on 2014-09-09)

Let G be a grammar that contains no left-recursive rules, and we use a recursive-descent recognizer that uses full backtracking, using list of results for example, to recognize strings of G.

How can someone show formally that if s is a sentence in G, then R(G), which is the
recognizer I just described for G, can recognize s, and it also explores all the paths, i.e., if there are two paths to recognition, both can be explored.

**Tags:** proofs, parsing, correctness

> **Comments:**
> **username_1**: Why do you want to do that rather than use dynamic programming which is more efficient, quadratic (for recognition only) rather than exponential, and can accept recursive rules? Also exploring all paths is useless for a recognizer: what is recognized is recognized.  
> **username_0**: My question here is not from a practicality point of view. You are right and there are indeed better options out there. I just would like to know how someone writes such proofs? How to show the correctness of a recursive-descent parser.  
> **username_1**: Not much time for it just now. Can you get inpiration from what is done to prove non-deterministic PDA recognize CF languages. After all, your backtrack  recursive-descent is just mimicking a non-deterministic PDA computation.  

---

## 0 answers

