Fundamenta Informaticae - Volume 149, issue 3

Authors: Abarca, M. | Rivera, D.

Article Type: Research Article

Abstract: A well known constructive proof for the 𝔸𝔻𝔼-classification of many mathematical objects, such as positive unit forms and their associated quasi-Cartan matrices, has lead to an Inflations Algorithm . However, this algorithm is not known to run in polynomial time. In this paper we use a so called flation transformation and show how its invariants can be used to characterize the Dynkin types 𝔸 and 𝔻 in the language of graph theory. Also, a polynomial-time algorithm for computing the Dynkin type is suggested.

Keywords: Positive unit forms, Dynkin-type, edge-bipartite graphs, combinatorial algorithms

DOI: 10.3233/FI-2016-1448

Citation: Fundamenta Informaticae, vol. 149, no. 3, pp. 241-261, 2016

Authors: Alessi, Fabio | Cardone, Felice

Article Type: Research Article

Abstract: We investigate the foundations of reasoning over infinite data structures by means of set-theoretical structures arising in the sheaf-theoretic semantics of higher-order intuitionistic logic. Our approach focuses on a natural notion of tiering involving an operation of restriction of elements to levels forming a complete Heyting algebra. We relate these tiered objects to final coalgebras and initial algebras of a wide class of endofunctors of the category of sets, and study their order and convergence properties. As a sample application, we derive a general proof principle for tiered objects.

Keywords: complete Heyting algebras, sheaves, initial algebras, final coalgebras, infinite data structures, approximation lemma

DOI: 10.3233/FI-2016-1449

Citation: Fundamenta Informaticae, vol. 149, no. 3, pp. 263-295, 2016

Authors: Bergstra, J.A. | Middelburg, C.A.

Article Type: Research Article

Abstract: Each Boolean function can be computed by a single-pass instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. Auxiliary Boolean registers are not necessary for this. In the current paper, we show that, in the case of the parity functions, shorter instruction sequences are possible with the use of an auxiliary Boolean register in the presence of instructions to complement the content of auxiliary Boolean registers. This result supports, in a setting where programs are instruction sequences acting on Boolean registers, a basic intuition behind the storage …of auxiliary data, namely the intuition that this makes possible a reduction of the size of a program. The work presented in this paper is carried out in the setting of PGA (ProGram Algebra) Show more

Keywords: Boolean function family, instruction sequence size, non-uniform complexity measure, parity function

DOI: 10.3233/FI-2016-1450

Citation: Fundamenta Informaticae, vol. 149, no. 3, pp. 297-309, 2016

Authors: Champarnaud, Jean-Marc | Mignot, Ludovic | Nicart, Florent

Article Type: Research Article

Abstract: This paper proposes an extension to classical regular expressions by the addition of two operators allowing the inclusion of boolean formulae from the zeroth order logic. These expressions are called constrained expressions . The associated language is defined thanks to the notion of interpretation and of realization. We show that the language associated when both interpretation and realization are fixed is stricly regular and can be not regular otherwise. Furthermore, we use an extension of Antimirov’s partial derivatives in order to solve the membership test in the general case. Finally, we show that once the interpretation is fixed, …the membership test of a word in the language denoted by a constrained expression can be undecidable whereas it is always decidable when the interpretation is not fixed. Show more

Keywords: Expression Derivatives, Constrained Expression, Zeroth Order Logic

DOI: 10.3233/FI-2016-1451

Citation: Fundamenta Informaticae, vol. 149, no. 3, pp. 311-361, 2016