Recursive Path Orderings Can Also Be Incremental

2005 ◽  
pp. 230-245 ◽  
Author(s):  
Mirtha-Lina Fernández ◽  
Guillem Godoy ◽  
Albert Rubio
Keyword(s):  
Recursive Path

scholarly journals A proof-theoretic study of abstract termination principles

2019 ◽  
Vol 29 (8) ◽  
pp. 1345-1366 ◽  
Author(s):  
Thomas Powell
Keyword(s):  
Complexity Analysis ◽  
Theoretic Analysis ◽  
Rewrite Systems ◽  
Abstract Setting ◽  
Term Rewrite Systems ◽  
Recursive Path

Abstract We carry out a proof-theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees that can be defined in Gödel’s system T plus bar recursion. We then carry out a complexity analysis of these terms and demonstrate how this can be applied to bound the derivational height of term rewrite systems.

scholarly journals Recursive Path Model for Health Literacy: The Effect of Social Support and Geographical Residence

2021 ◽  
Vol 9 ◽  
Author(s):  
Éva Bíró ◽  
Ferenc Vincze ◽  
Gabriella Mátyás ◽  
Karolina Kósa
Keyword(s):  
Social Support ◽  
Health Literacy ◽  
Educational Attainment ◽  
Rural Areas ◽  
Path Model ◽  
Determinants Of Health ◽  
Sociodemographic Variables ◽  
Permanent Residence ◽  
Improve Health ◽  
Recursive Path

Background: The public health relevance of health literacy is highlighted by the fact that its higher levels can improve health outcomes and reduce health inequities. In order to design effective interventions for improving health literacy, the relationship between health literacy and other factors such as sociodemographic variables, subjective health and social support must be understood.Objective: Our aim was to test a socioecological model of the determinants of health literacy with a special focus on the effect of residence. Our study investigated geographical differences regarding the levels of health literacy and its determinants as this was not investigated before in European nationwide surveys.Methods: Data was collected by a polling company in a sample (n = 1,200) of the Hungarian adult population nationally representative by age, gender, and permanent residence in 2019 January. The questionnaire included items on sociodemographic data, subjective well-being, social support, and two health literacy scales. A recursive path model was used to outline the mediating effect of social support between sociodemographic variables and health literacy where both direct and indirect effects of the explanatory variables and multiple relationships among the variables were analyzed simultaneously. Multiple-group analysis was applied to the three pre-set categories of permanent residence (capital city, urban and rural).Results: There was no statistically significant difference by residence regarding levels of health literacy. Social support and educational attainment were the most important determinants of health literacy after adjusting for the effect of other sociodemographic variables. However, the magnitude of effect of social support and educational attainment is different between types of settlements, the strongest being in rural areas.Conclusion: Social support seems to mediate the effect of socioeconomic position on health literacy which could be taken into account when designing interventions to improve health literacy, especially in rural areas. Further studies would be needed especially in rural communities to see whether improvement of social support could be utilized in projects to increase the level of health literacy.

scholarly journals SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs

2010 ◽  
Vol 49 (1) ◽  
pp. 53-93 ◽  
Author(s):  
Michael Codish ◽  
Jürgen Giesl ◽  
Peter Schneider-Kamp ◽  
René Thiemann
Keyword(s):  
Sat Solving ◽  
Dependency Pairs ◽  
Termination Proofs ◽  
Recursive Path

scholarly journals On recursive path ordering

1985 ◽  
Vol 40 ◽  
pp. 323-328 ◽  
Author(s):  
M.S. Krishnamoorthy ◽  
P. Narendran
Keyword(s):  
Path Ordering ◽  
Recursive Path

Termination of rewriting in the Calculus of Constructions

2003 ◽  
Vol 13 (2) ◽  
pp. 339-414 ◽  
Author(s):  
DARIA WALUKIEWICZ-CHRZĄSZCZ
Keyword(s):  
Lambda Calculus ◽  
Term Rewriting ◽  
Higher Order ◽  
Strong Normalization ◽  
Term Rewriting System ◽  
Calculus Of Constructions ◽  
Path Ordering ◽  
Higher Order Functions ◽  
Rewriting Rules ◽  
Recursive Path

We show how to incorporate rewriting into the Calculus of Constructions and we prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. An important novelty of this paper is the possibility to define rewriting rules over dependently typed function symbols. We prove strong normalization for any term rewriting system, such that all function symbols satisfy the, so called, star dependency condition, and every rule is accepted by the Higher Order Recursive Path Ordering (which is an extension of the method created by Jouannaud and Rubio for the setting of the simply typed lambda calculus). The proof of strong normalization is done by using a typed version of reducibility candidates due to Coquand and Gallier. Our criterion is general enough to accept definitions by rewriting of many well-known higher order functions, for example dependent recursors for inductive types or proof carrying functions. This makes it a very good candidate for inclusion in a proof assistant based on the Curry-Howard isomorphism.

Sign in / Sign up

Export Citation Format

Share Document