The Experts below are selected from a list of 36 Experts worldwide ranked by ideXlab platform

Rogério Reis - One of the best experts on this subject based on the ideXlab platform.

  • The computational power of parsing expression grammars
    arXiv: Formal Languages and Automata Theory, 2019
    Co-Authors: Bruno Loff, Nelma Moreira, Rogério Reis
    Abstract:

    We study the computational power of parsing expression grammars (PEGs). We begin by constructing PEGs with unexpected behaviour, and surprising new examples of languages with PEGs, including the language of palindromes whose length is a power of two, and a binary-counting language. We then propose a new computational model, the scaffolding automaton, and prove that it exactly characterises the computational power of parsing expression grammars (PEGs). Using this characterisation we show that: (*) PEGs have unexpected power and semantics. We present several PEGs with surprising behaviour, and languages which, unexpectedly, have PEGs, including a PEG for the language of palindromes whose length is a power of two. (*) PEGs are computationally `universal', in the following sense: take any Computable Function $f:\{0,1\}^\ast\to \{0,1\}^\ast$; then there exists a Computable Function $g: \{0,1\}^\ast \to \mathbb{N}$ such that $\{ f(x) \#^{g(x)} x \mid x \in \{0,1\}^\ast \}$ has a PEG. (*) There can be no pumping lemma for PEGs. There is no Total Computable Function $A$ with the following property: for every well-formed PEG $G$, there exists $n_0$ such that for every string $x \in \mathcal{L}(G)$ of size $|x| \ge n_0$, the output $y = A(G, x)$ is in $\mathcal{L}(G)$ and has $|y| > |x|$. (*) PEGs are strongly non real-time for Turing machines. There exists a language with a PEG, such that neither it nor its reverse can be recognised by any multi-tape online Turing machine which is allowed to do only $o(n/\log n)$ steps after reading each input symbol.

  • DLT - The Computational Power of Parsing Expression Grammars
    Developments in Language Theory, 2018
    Co-Authors: Bruno Loff, Nelma Moreira, Rogério Reis
    Abstract:

    We propose a new computational model, the scaffolding automaton, which exactly characterises the computational power of parsing expression grammars (PEGs). Using this characterisation we show that: PEGs have unexpected power and semantics. We present several PEGs with surprising behaviour, and languages which, unexpectedly, have PEGs, including a PEG for the language of palindromes whose length is a power of two. PEGs are computationally “universal”, in the following sense: take any Computable Function \(f:\{0, 1\}^*\rightarrow \{0, 1\}^*\); then there exists a Computable Function \(g: \{0, 1\}^*\rightarrow {\mathbb {N}}\) such that \(\{ f(x) \#^{g(x)} x \mid x \in \{0, 1\}^*\}\) has a PEG. There can be no pumping lemma for PEGs. There is no Total Computable Function A with the following property: for every well-formed PEG G, there exists \(n_0\) such that for every string \(x \in {\mathcal {L}}(G)\) of size \(|x| \ge n_0\), the output \(y = A(G, x)\) is in \({\mathcal {L}}(G)\) and has \(|y| > |x|\). PEGs are strongly non real-time for Turing machines. There exists a language with a PEG, such that neither it nor its reverse can be recognised by any multi-tape online Turing machine which is allowed to do only \(o(n/\log n)\) steps after reading each input symbol.

Bruno Loff - One of the best experts on this subject based on the ideXlab platform.

  • The computational power of parsing expression grammars
    arXiv: Formal Languages and Automata Theory, 2019
    Co-Authors: Bruno Loff, Nelma Moreira, Rogério Reis
    Abstract:

    We study the computational power of parsing expression grammars (PEGs). We begin by constructing PEGs with unexpected behaviour, and surprising new examples of languages with PEGs, including the language of palindromes whose length is a power of two, and a binary-counting language. We then propose a new computational model, the scaffolding automaton, and prove that it exactly characterises the computational power of parsing expression grammars (PEGs). Using this characterisation we show that: (*) PEGs have unexpected power and semantics. We present several PEGs with surprising behaviour, and languages which, unexpectedly, have PEGs, including a PEG for the language of palindromes whose length is a power of two. (*) PEGs are computationally `universal', in the following sense: take any Computable Function $f:\{0,1\}^\ast\to \{0,1\}^\ast$; then there exists a Computable Function $g: \{0,1\}^\ast \to \mathbb{N}$ such that $\{ f(x) \#^{g(x)} x \mid x \in \{0,1\}^\ast \}$ has a PEG. (*) There can be no pumping lemma for PEGs. There is no Total Computable Function $A$ with the following property: for every well-formed PEG $G$, there exists $n_0$ such that for every string $x \in \mathcal{L}(G)$ of size $|x| \ge n_0$, the output $y = A(G, x)$ is in $\mathcal{L}(G)$ and has $|y| > |x|$. (*) PEGs are strongly non real-time for Turing machines. There exists a language with a PEG, such that neither it nor its reverse can be recognised by any multi-tape online Turing machine which is allowed to do only $o(n/\log n)$ steps after reading each input symbol.

  • DLT - The Computational Power of Parsing Expression Grammars
    Developments in Language Theory, 2018
    Co-Authors: Bruno Loff, Nelma Moreira, Rogério Reis
    Abstract:

    We propose a new computational model, the scaffolding automaton, which exactly characterises the computational power of parsing expression grammars (PEGs). Using this characterisation we show that: PEGs have unexpected power and semantics. We present several PEGs with surprising behaviour, and languages which, unexpectedly, have PEGs, including a PEG for the language of palindromes whose length is a power of two. PEGs are computationally “universal”, in the following sense: take any Computable Function \(f:\{0, 1\}^*\rightarrow \{0, 1\}^*\); then there exists a Computable Function \(g: \{0, 1\}^*\rightarrow {\mathbb {N}}\) such that \(\{ f(x) \#^{g(x)} x \mid x \in \{0, 1\}^*\}\) has a PEG. There can be no pumping lemma for PEGs. There is no Total Computable Function A with the following property: for every well-formed PEG G, there exists \(n_0\) such that for every string \(x \in {\mathcal {L}}(G)\) of size \(|x| \ge n_0\), the output \(y = A(G, x)\) is in \({\mathcal {L}}(G)\) and has \(|y| > |x|\). PEGs are strongly non real-time for Turing machines. There exists a language with a PEG, such that neither it nor its reverse can be recognised by any multi-tape online Turing machine which is allowed to do only \(o(n/\log n)\) steps after reading each input symbol.

Nelma Moreira - One of the best experts on this subject based on the ideXlab platform.

  • The computational power of parsing expression grammars
    arXiv: Formal Languages and Automata Theory, 2019
    Co-Authors: Bruno Loff, Nelma Moreira, Rogério Reis
    Abstract:

    We study the computational power of parsing expression grammars (PEGs). We begin by constructing PEGs with unexpected behaviour, and surprising new examples of languages with PEGs, including the language of palindromes whose length is a power of two, and a binary-counting language. We then propose a new computational model, the scaffolding automaton, and prove that it exactly characterises the computational power of parsing expression grammars (PEGs). Using this characterisation we show that: (*) PEGs have unexpected power and semantics. We present several PEGs with surprising behaviour, and languages which, unexpectedly, have PEGs, including a PEG for the language of palindromes whose length is a power of two. (*) PEGs are computationally `universal', in the following sense: take any Computable Function $f:\{0,1\}^\ast\to \{0,1\}^\ast$; then there exists a Computable Function $g: \{0,1\}^\ast \to \mathbb{N}$ such that $\{ f(x) \#^{g(x)} x \mid x \in \{0,1\}^\ast \}$ has a PEG. (*) There can be no pumping lemma for PEGs. There is no Total Computable Function $A$ with the following property: for every well-formed PEG $G$, there exists $n_0$ such that for every string $x \in \mathcal{L}(G)$ of size $|x| \ge n_0$, the output $y = A(G, x)$ is in $\mathcal{L}(G)$ and has $|y| > |x|$. (*) PEGs are strongly non real-time for Turing machines. There exists a language with a PEG, such that neither it nor its reverse can be recognised by any multi-tape online Turing machine which is allowed to do only $o(n/\log n)$ steps after reading each input symbol.

  • DLT - The Computational Power of Parsing Expression Grammars
    Developments in Language Theory, 2018
    Co-Authors: Bruno Loff, Nelma Moreira, Rogério Reis
    Abstract:

    We propose a new computational model, the scaffolding automaton, which exactly characterises the computational power of parsing expression grammars (PEGs). Using this characterisation we show that: PEGs have unexpected power and semantics. We present several PEGs with surprising behaviour, and languages which, unexpectedly, have PEGs, including a PEG for the language of palindromes whose length is a power of two. PEGs are computationally “universal”, in the following sense: take any Computable Function \(f:\{0, 1\}^*\rightarrow \{0, 1\}^*\); then there exists a Computable Function \(g: \{0, 1\}^*\rightarrow {\mathbb {N}}\) such that \(\{ f(x) \#^{g(x)} x \mid x \in \{0, 1\}^*\}\) has a PEG. There can be no pumping lemma for PEGs. There is no Total Computable Function A with the following property: for every well-formed PEG G, there exists \(n_0\) such that for every string \(x \in {\mathcal {L}}(G)\) of size \(|x| \ge n_0\), the output \(y = A(G, x)\) is in \({\mathcal {L}}(G)\) and has \(|y| > |x|\). PEGs are strongly non real-time for Turing machines. There exists a language with a PEG, such that neither it nor its reverse can be recognised by any multi-tape online Turing machine which is allowed to do only \(o(n/\log n)\) steps after reading each input symbol.

Steve Reeves - One of the best experts on this subject based on the ideXlab platform.

  • Supporting students' work in a formal system: MacPICT
    2007
    Co-Authors: Steve Reeves
    Abstract:

    MacPICT is an interactive program written in LPA Prolog which has encoded within it the rules of Martin-Lof's constructive type theory (CTT), a formal system based on the constructive or intuitionistic mathematics of Brouwer, Heyting and others. It allows us to specify and express any Total, Computable Function, so from a computer science point of view we can write both specifications and programs, along with the derivations which lead from one to the other, in a single language. MacPICT is a reconstruction of PICT [Ham92] and is intended to support the teaching of CTT. It has been developed and improved over the last five years, during which time it has been used to support teaching in an M.Sc. course on CTT at QMW. Many of the developments and improvements were suggested by students since they used the system to work on substantial courseworks. As we shall see, MacPICT can be used to assist in the development of derivations in CTT and so it is called a derivation assistant (DA). In this paper I show how MacPICT can be used for supporting derivations in CTT and consider what current experience suggests for future improvement. The examples in this paper will not require any knowledge of CTT since the meaning will either be clear to anyone with experience of logic and programming notations in general or will be explained as necessary.

  • Computer support for students’ work in a formal system: MacCPICT
    International Journal of Mathematical Education in Science and Technology, 1995
    Co-Authors: Steve Reeves
    Abstract:

    MacPICT is an interactive program written in LPA Prolog which has encoded within it the rules of Martin‐L#auof’ s constructive type theory #opCTT#cp, a formal system based on constructive or intuitionistic mathematics. It allows us to specify and express any Total, Computable Function, so from a computer science point of view we can write both specifications and programs, along with the derivations which lead from one to the other, in a single language. It can also be used, via the ‘logical’ interpretation, to support construction of derivations in a course which teaches intuitionistic, propositional, first‐ or higher‐order logic. MacPICT is a reconstruction of PICT #ob1#cb and is intended to support the teaching of CTT. It has been developed and improved over the last five years, during which time it has been used to support teaching in an MSc. course. In this paper I show how MacPICT can be used for supporting derivations in CTT, by way of detailed examples, and suggest some further problems the reader ...

  • A calculator for supporting derivation in constructive type-theory: PICTCalc
    1994
    Co-Authors: Steve Reeves
    Abstract:

    PICTCalc is an interactive program written in LPA Prolog which has encoded within it the rules of Martin-Lof's constructive type theory (CTT), a formal system based on the constructive or intuitionistic mathematics of Brouwer, Heyting and others. It allows us to specify and express any Total, Computable Function, so from a computer science point of view we can write both specifications and programs, along with the derivations which lead from one to the other, in a single language. PICTCalc is a more recent version of MacPICT which is itself a reconstruction of PICT [Ham92] and is intended as a test-bed for providing formal support for work within CTT. It has been developed and improved over the last five years, during which time it has been used to support teaching in an M.Sc. course on CTT at QMW. Many of the developments and improvements were suggested by students since they used the system to work on substantial courseworks. As we shall see, PICTCalc can be used to assist in the development of derivations in CTT and so it is called a derivation assistant (DA). In this paper I show how PICTCalc can be used for supporting derivations in CTT and consider what current experience suggests for future improvement. The examples in this paper will not require any knowledge of CTT since the meaning will either be clear to anyone with experience of logic and programming notations in general or will be explained as necessary.

Simonsen, Jakob Grue - One of the best experts on this subject based on the ideXlab platform.

  • Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus
    Springer Verlag, 2010
    Co-Authors: Ketema Jeroen, Simonsen, Jakob Grue
    Abstract:

    We study the Church-Rosser property - which is also known as confluence - in term rewriting and λ-calculus. Given a system R and a peak t *← s →* t' in R, we are interested in the length of the reductions in the smallest corresponding valley t →* s' *← t' as a Function vs_R(m,n) of the size m of s and the maximum length n of the reductions in the peak. For confluent term rewriting systems (TRSs), we prove the (expected) result that vs_R(m,n) is a Computable Function. Conversely, for every Total Computable Function φ(n) there is a TRS with a single term s such that vs_R(|s|,n) ≥ φ(n) for all n. In contrast, for orthogonal term rewriting systems R we prove that there is a constant k such that vs_R(m,n) is bounded from above by a Function exponential in k and independent of the size of s. For λ-calculus, we show that vs_R(m,n) is bounded from above by a Function contained in the fourth level of the Grzegorczyk hierarchy