The Church-Rosser property in dual combinatory logic

2003 ◽  
Vol 68 (1) ◽  
pp. 132-152 ◽  
Author(s):  
Katalin Bimbó
Keyword(s):  
General Theorem ◽  
Combinatory Logic ◽  
Unique Decomposition ◽  
Per Se ◽  
Structurally Free Logics ◽  
The Church

AbstractDual combinators emerge from the aim of assigning formulas containing ← as types to combinators. This paper investigates formally some of the properties of combinatory systems that include both combinators and dual combinators. Although the addition of dual combinators to a combinatory system does not affect the unique decomposition of terms, it turns out that some terms might be redexes in two ways (with a combinator as its head, and with a dual combinator as its head). We prove a general theorem stating that no dual combinatory system possesses the Church-Rosser property. Although the lack of confluence might be problematic in some cases, it is not a problem per se. In particular, we show that no damage is inflicted upon the structurally free logics, the system in which dual combinators first appeared.

TERMINATION OF ABSTRACT REDUCTION SYSTEMS

2009 ◽  
Vol 20 (01) ◽  
pp. 57-82
Author(s):  
JEREMY E. DAWSON ◽  
RAJEEV GORÉ
Keyword(s):  
General Theorem ◽  
Combinatory Logic ◽  
Rewrite Systems ◽  
Path Ordering

We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.

What is Distinctive about Methodist Ecclesiology? A Response to Papers by Miriam Haar, Justus Hunter and Robert Martin

Ecclesiology ◽  
2013 ◽  
Vol 9 (1) ◽  
pp. 66-74
Author(s):  
Kenneth Wilson
Keyword(s):  
Catholic Church ◽  
Church Of England ◽  
Roman Catholic ◽  
The Body ◽  
Roman Catholic Church ◽  
Body Of Christ ◽  
Per Se ◽  
The Church

Does Methodism want a distinctive ecclesiology? British Methodism assumes its ecclesiology from the Church of England which explains its lack of ecclesiological thinking, its genuine desire for reunification, and indeed its focus on ecclesia in actu. But there can be no ecclesia in actu apart from ecclesia per se. Being and doing are one in God. The Church, grounded in the dynamic being of God in Trinity, celebrates in the action of the Eucharist the wholeness of God’s presence with his world. Proleptically the Church includes the whole of creation and all people. Hence, when as the Body of Christ we pray the Our Father with our Lord, we pray on behalf of all, not just for ourselves. But what then do we mean by apostolicity? Perhaps in Methodism we would be well occupied exploring more keenly with the Roman Catholic Church what we each mean by being a society within the church. Outler may have been right when he opined that Methodism needed a Catholic Church within which to be church.

Wittenberg Reformers

2021 ◽  
pp. 27-51
Author(s):  
Esther Chung-Kim
Keyword(s):  
Catholic Church ◽  
Central Component ◽  
Poor Relief ◽  
System P ◽  
Theological Foundations ◽  
The Common ◽  
Per Se ◽  
Relief System ◽  
Mendicant Orders ◽  
The Church

Wittenberg reformers supported the transfer of formerly Catholic Church properties to government possession. This secularization of church property did not mean a rejection of religion per se; on the contrary, secularization of church property meant that political rulers consolidated the scattered ecclesiastical properties and possessions into a common chest so that they could support the reform of the church. While Martin Luther and Andreas Karlstadt denounced mendicant orders for their begging lifestyle, they called for cities to care for their resident poor so that begging would be obsolete. Their critique became the catalyst for change, including an educated pastorate with preaching as a central component of worship, schools for boys and girls, and a system of poor relief funded by monastic foundations, confraternities, and donations. In the transfer of property to the common chest, Wittenberg reformers were crucial in providing the theological foundations for the transition to a centralized poor relief system.

Defining Catholicism

2018 ◽  
Author(s):  
Natalia Nowakowska
Keyword(s):  
World View ◽  
The Past ◽  
Language Analysis ◽  
Per Se ◽  
The Church ◽  
Chief Characteristic ◽  
Large Corpus

This discussion asks what King Sigismund of Poland and his subjects understood catholicism to be in the 1520s and 1530s, through language analysis of a diverse and large corpus of sources. It finds that (in contrast to ‘luteranismus’) there was no name for catholicism per se. The church was defined primarily with reference to the past: as the church of one’s ancestors, of the Fathers, of many past centuries. Its chief characteristic was its (alleged) historic unity, resting on a carefully preserved consensus down the ages. Under the pressure of events, however, we find the language used by catholics in Poland-Prussia shifting, from a pre-confessional universal world view towards proto-confessional positions: from ‘good and bad Christians’ to ‘Catholic’ versus ‘Lutheran’. Reformation supporters, meanwhile, described this church very differently—as papal-led, built on distinctive doctrinal positions, and located in a dead, rather than a living, past.

GENDER IN YORUBA RELIGIOUS CHANGE

2002 ◽  
Vol 32 (2) ◽  
pp. 136-166 ◽  
Author(s):  
Keyword(s):  
Religious Practice ◽  
Early Church ◽  
Church Membership ◽  
Religious Change ◽  
Congregational Life ◽  
The Social ◽  
Church Life ◽  
Per Se ◽  
Indigenous Society ◽  
The Church

AbstractThis paper explores the relevance of gender to the reception of Christianity and to early church life in nineteenth-century Yorubaland. These were profoundly shaped by the gender conceptions prevalent in indigenous society and religion. Though the indigenous gods (orisa) lacked gender as a fixed or intrinsic attribute, gender conceptions were projected on to them. Witchcraft was mostly attributed to women both as its victims and as its perpetrators, and with men and ancestral cults chiefly responsible for its control. There was an overlap between the social placement of witches and Christian converts, both being relatively marginal. Religious practice was also strongly gendered, with women preponderant in the cult of most orisa, but men in the main oracular cult, Ifa. Women found something of an equivalent in the cult of Ori, or personal destiny. The missions initially met their readiest response among young men, who were less tied to the orisa cults than women were. By the second generation the balance shifted, as male prestige values were incompatible with full church membership and women came more to the fore in congregational life. As an aspect of this, the church took on many of the concerns that the orisa cults had offered women—a token of this being the honorific use of the term 'mother'. In the end it is less gender per se than the gender/age conjunction that is critical.

Strong reduction and normal form in combinatory logic

1967 ◽  
Vol 32 (2) ◽  
pp. 213-223 ◽  
Author(s):  
Bruce Lercher
Keyword(s):  
Normal Form ◽  
Combinatory Logic ◽  
Strong Reduction ◽  
The Church

The notion of strong reduction is introduced in Curry and Feys' book Combinatory logic [1] as an analogue, in the theory of combinatore, to reduction (more exactly, βη-reduction) in the theory of λ-conversion. The existence of an analogue and its possible importance are suggested by an equivalence between the theory of combinatore and λ-conversion, and the Church-Rosser theorem in λ-conversion. This theorem implies that if a formula X is convertible to a formula X* which cannot be further reduced—is irreducible, or in normal form—then X is convertible to X* by a reduction alone. Moreover, the reduction may be performed in a certain prescribed order.

BROAD-CHURCH HOMILETICS, KINGSLEY'SHYPATIA, AND THE CULTIVATED READER IN THE PEW

2016 ◽  
Vol 44 (3) ◽  
pp. 491-509
Author(s):  
Daniel Cook
Keyword(s):  
Nineteenth Century ◽  
Charles Kingsley ◽  
Freedom Of Conscience ◽  
Social Mission ◽  
The Social ◽  
Scientific Mind ◽  
Per Se ◽  
The Church ◽  
Vast Range ◽  
Looking Back

The first issue and numberof theNineteenth Century, 1877, included a searching article by J. Baldwin Brown entitled “Is the Pulpit Losing Its Power?” Looking back over the decades, Brown marked a generational decline in England's preaching, which he argued had now been eclipsed by a print market distributing “freest discussion of the most sacred truths.” Brown lamented that fewer talented men now joined the Anglican ministry, while the Church had increasingly withdrawn from the social mission which had animated mid-century preachers like Charles Kingsley (107–09). More troublingly, Brown speculated that modern Britons had become constitutionally averse to the homiletic situation. The preacher, he writes, often “seems as if he came down on the vast range of subjects which he is tempted to handle as from a superior height; and this is what the scientific mind can never endure. . . . [T]here has always been a sort of omniscient tone in the pulpit method of handling intellectual questions which stirs fierce rebellion in cultivated minds and hearts” (109–10). Brown pulls up short of blaming theology per se; for him its language of “above” and “beyond” has continuing relevance (110). Still, he broaches the possibility that by its very nature preaching risks antagonizing what current scholarship would term the “liberal subject”: one which prizes freedom of conscience, empirical exploration, and debate.

Gifts in Frankalmoign, Warranty of Land, and Feudal Society

1991 ◽  
Vol 50 (2) ◽  
pp. 330-346 ◽  
Author(s):  
David Postles
Keyword(s):  
Twelfth Century ◽  
Personal Relationship ◽  
Recent Discussion ◽  
Legal Norms ◽  
Feudal Society ◽  
The Future ◽  
Per Se ◽  
The One ◽  
The Mind ◽  
The Church

In recent discussion, gifts to the religious have been perceived as exercising a formative influence in the forging of some norms and customs of feudal tenure during the twelfth century. On the one hand, it has been suggested that gifts to the church assisted the clarification in the mind of lay feudal society of the concept of heritability—that is, the future enjoyment of inheritance—since donors could not alienate in perpetuity that which was not already heritable. This suggestion is extremely important in view of the different perceptions of political and legal historians concerning the development of heritability of tenures and tenant right during the twelfth century, which are seen variously to have existed as social or legal norms from varying times and from different causes. A related argument runs that, whilst the warranty clause in charters (but not warranty per se) was initially conceived within the framework of the personal relationship between lord and man, its more widespread diffusion in charters was stimulated largely through the auspices of these religious beneficiaries of gifts in frankalmoign. The introduction of warranty into charters at the instance of religious beneficiaries is thus related to their concern to secure their own perpetual rights in the land at a time of a nascent realisation of hereditary tenant right, and the religious were thus foremost in the insertion of warranty clauses in charters which they, as beneficiaries, wrote or influenced, to secure their own unbridled tenure in perpetuity.

The Church-Rosser property in symmetric combinatory logic

2005 ◽  
Vol 70 (2) ◽  
pp. 536-556 ◽  
Author(s):  
Katalin Bimbó
Keyword(s):  
Fixed Point ◽  
Place Identity ◽  
Combinatory Logic ◽  
Left And Right ◽  
The One ◽  
The Church

AbstractSymmetic combinatory logic with the symmetric analogue of a combinatorially complete base (in the form of symmetric λ-calculus) is known to lack the Church-Rosser property. We prove a much stronger theorem that no symmetric combinatory logic that contains at least two proper symmetric combinatory has the Church-Rosser property. Although the statement of the result looks similar to an earlier one concerning dual combinatory logic, the proof is different because symmetric combinators may form redexes in both left and right associated terms. Perhaps surprisingly, we are also able to show that certain symmetric combinatory logics that include just one particular constant are not confluent. This result (beyond other differences) clearly sets apart symmetric combinatory logic from dual combinatory logic, since all dual combinatory systems with a single combinator or a single dual combinator are Church-Rosser. Lastly, we prove that a symmetric combinatory logic that contains the fixed point and the one-place identity combinator has the Church-Rosser property.

Sign in / Sign up

Export Citation Format

Share Document