Control Problem of a Class of Pushdown Automata Based on <I>Posets</I> and Its Application to Resolution Deductions

Susumu YAMASAKI

Control Problem of a Class of Pushdown Automata Based on Posets and Its Application to Resolution Deductions

Susumu YAMASAKI

Full Text Views

0

Cite this

Summary :

In this paper, a pushdown automaton, with an infinite set of states as a partially ordered set (poset), is formulated, and its control problem of whether a given configuration can be transferred to another is discussed. For the controllability to be decidable, we take a condition the poset satisfies, that is, a condition that there are only finite number of states under the partial ordering between two given states. The control problem is decidable in polynomial time on condition the length of each pushed stack string is bounded by a constant in a given pushdown automaton. The motivation of considering the control problem comes up from the stack structure in implementing the SLD resolution deductions, in which the leftmost atom in each goal is selected and unified with some procedure name (that is, some head) of a definite clause, with the effect of the procedure name being replaced by the procedure bodies and unifications. Thus, the control problem is applied to describe the SLD resolution deductions of finite steps, by constructing a pushdown automaton model for a set of definite clauses, in which leftmost selection of atom in each goal forms a stack structure and substitutions affecting goals are interpreted as states. When constructing a pushdown automaton model for an SLD resolution deduction, algebraic properties of the idempotent substitution set, which are used in unifications, are examined and utilized. The quotient set of the idempotent substitution set per renamings is adopted to present the automaton model.

Publication: IEICE TRANSACTIONS on Information Vol.E78-D No.11 pp.1488-1497

Publication Date: 1995/11/25

Publicized

Online ISSN

DOI

Type of Manuscript: PAPER

Category: Automata, Languages and Theory of Computing

Cite this

Copy

Susumu YAMASAKI, "Control Problem of a Class of Pushdown Automata Based on Posets and Its Application to Resolution Deductions" in IEICE TRANSACTIONS on Information, vol. E78-D, no. 11, pp. 1488-1497, November 1995, doi: .
Abstract: In this paper, a pushdown automaton, with an infinite set of states as a partially ordered set (poset), is formulated, and its control problem of whether a given configuration can be transferred to another is discussed. For the controllability to be decidable, we take a condition the poset satisfies, that is, a condition that there are only finite number of states under the partial ordering between two given states. The control problem is decidable in polynomial time on condition the length of each pushed stack string is bounded by a constant in a given pushdown automaton. The motivation of considering the control problem comes up from the stack structure in implementing the SLD resolution deductions, in which the leftmost atom in each goal is selected and unified with some procedure name (that is, some head) of a definite clause, with the effect of the procedure name being replaced by the procedure bodies and unifications. Thus, the control problem is applied to describe the SLD resolution deductions of finite steps, by constructing a pushdown automaton model for a set of definite clauses, in which leftmost selection of atom in each goal forms a stack structure and substitutions affecting goals are interpreted as states. When constructing a pushdown automaton model for an SLD resolution deduction, algebraic properties of the idempotent substitution set, which are used in unifications, are examined and utilized. The quotient set of the idempotent substitution set per renamings is adopted to present the automaton model.
URL: https://global.ieice.org/en_transactions/information/10.1587/e78-d_11_1488/_p

Copy

@ARTICLE{e78-d_11_1488,
author={Susumu YAMASAKI, },
journal={IEICE TRANSACTIONS on Information},
title={Control Problem of a Class of Pushdown Automata Based on Posets and Its Application to Resolution Deductions},
year={1995},
volume={E78-D},
number={11},
pages={1488-1497},
abstract={In this paper, a pushdown automaton, with an infinite set of states as a partially ordered set (poset), is formulated, and its control problem of whether a given configuration can be transferred to another is discussed. For the controllability to be decidable, we take a condition the poset satisfies, that is, a condition that there are only finite number of states under the partial ordering between two given states. The control problem is decidable in polynomial time on condition the length of each pushed stack string is bounded by a constant in a given pushdown automaton. The motivation of considering the control problem comes up from the stack structure in implementing the SLD resolution deductions, in which the leftmost atom in each goal is selected and unified with some procedure name (that is, some head) of a definite clause, with the effect of the procedure name being replaced by the procedure bodies and unifications. Thus, the control problem is applied to describe the SLD resolution deductions of finite steps, by constructing a pushdown automaton model for a set of definite clauses, in which leftmost selection of atom in each goal forms a stack structure and substitutions affecting goals are interpreted as states. When constructing a pushdown automaton model for an SLD resolution deduction, algebraic properties of the idempotent substitution set, which are used in unifications, are examined and utilized. The quotient set of the idempotent substitution set per renamings is adopted to present the automaton model.},
keywords={},
doi={},
ISSN={},
month={November},}

Copy

TY - JOUR
TI - Control Problem of a Class of Pushdown Automata Based on Posets and Its Application to Resolution Deductions
T2 - IEICE TRANSACTIONS on Information
SP - 1488
EP - 1497
AU - Susumu YAMASAKI
PY - 1995
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E78-D
IS - 11
JA - IEICE TRANSACTIONS on Information
Y1 - November 1995
AB - In this paper, a pushdown automaton, with an infinite set of states as a partially ordered set (poset), is formulated, and its control problem of whether a given configuration can be transferred to another is discussed. For the controllability to be decidable, we take a condition the poset satisfies, that is, a condition that there are only finite number of states under the partial ordering between two given states. The control problem is decidable in polynomial time on condition the length of each pushed stack string is bounded by a constant in a given pushdown automaton. The motivation of considering the control problem comes up from the stack structure in implementing the SLD resolution deductions, in which the leftmost atom in each goal is selected and unified with some procedure name (that is, some head) of a definite clause, with the effect of the procedure name being replaced by the procedure bodies and unifications. Thus, the control problem is applied to describe the SLD resolution deductions of finite steps, by constructing a pushdown automaton model for a set of definite clauses, in which leftmost selection of atom in each goal forms a stack structure and substitutions affecting goals are interpreted as states. When constructing a pushdown automaton model for an SLD resolution deduction, algebraic properties of the idempotent substitution set, which are used in unifications, are examined and utilized. The quotient set of the idempotent substitution set per renamings is adopted to present the automaton model.
ER -