Search results for 'Combinatory logic' (try it on Scholar)

1000+ found
Sort by:
  1. Katalin Bombó (2005). The Church-Rosser Property in Symmetric Combinatory Logic. Journal of Symbolic Logic 70 (2):536 - 556.score: 186.0
    Symmetic 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 combinators 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 (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. M. W. Bunder & W. J. M. Dekkers (2005). Equivalences Between Pure Type Systems and Systems of Illative Combinatory Logic. Notre Dame Journal of Formal Logic 46 (2):181-205.score: 186.0
    Pure Type Systems, PTSs, were introduced as a generalization of the type systems of Barendregt's lambda cube and were designed to provide a foundation for actual proof assistants which will verify proofs. Systems of illative combinatory logic or lambda calculus, ICLs, were introduced by Curry and Church as a foundation for logic and mathematics. In an earlier paper we considered two changes to the rules of the PTSs which made these rules more like ICL rules. This led (...)
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  3. Jean-Pierre Desclés, Anca Christine Pascu & Hee-Jin Ro (forthcoming). Aspecto-Temporal Meanings Analysed by Combinatory Logic. Journal of Logic, Language and Information:1-22.score: 186.0
    What is the meaning of language expressions and how to compute or calculate it? In this paper, we give an answer to this question by analysing the meanings of aspects and tenses in natural languages inside the formal model of an grammar of applicative, cognitive and enunciative operations (GRACE) (Desclés and Ro in Math Sci Hum 194:39–70, 2011), using the applicative formalism, functional types of categorial grammars and combinatory logic (CL) (Curry and Feys in Combinatory Logic. (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  4. Haskell B. Curry (1958). Combinatory Logic. Amsterdam, North-Holland Pub. Co..score: 180.0
    CHAPTER Addenda to Pure Combinatory Logic This chapter will treat various additions to, and modifications of, the subject matter of Chapters-7. ...
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  5. J. Roger Hindley (1972). Introduction to Combinatory Logic. Cambridge [Eng.]University Press.score: 180.0
    Introduction Combinatory logic deals with a class of formal systems designed for studying certain primitive ways in which functions can be combined to form ...
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. Katalin Bimbó (2012). Combinatory Logic: Pure, Applied, and Typed. Taylor & Francis.score: 150.0
    Reader-friendly without compromising the precision of exposition, the book includes many new research results not found in the available literature.
    Direct download  
     
    My bibliography  
     
    Export citation  
  7. Maarten Wicher Visser Bunder (1969). Set Theory Based on Combinatory Logic. Groningen, V. R. B. --Offsetdrukkerij (Kleine Der a 3-4).score: 150.0
    No categories
     
    My bibliography  
     
    Export citation  
  8. Frederic B. Fitch (1974). Elements of Combinatory Logic. New Haven,Yale University Press.score: 150.0
    No categories
     
    My bibliography  
     
    Export citation  
  9. Sören Stenlund (1971). Introduction to Combinatory Logic. Uppsala,Uppsala Universitetet, Filosofiska Föreningen Och Filosofiska Institutionen.score: 150.0
     
    My bibliography  
     
    Export citation  
  10. Andrea Cantini (2003). The Axiom of Choice and Combinatory Logic. Journal of Symbolic Logic 68 (4):1091-1108.score: 126.0
    We combine a variety of constructive methods (including forcing, realizability, asymmetric interpretation), to obtain consistency results concerning combinatory logic with extensionality and (forms of) the axiom of choice.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  11. Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic. Journal of Symbolic Logic 63 (3):869-890.score: 126.0
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  12. Henk Barendregt, Martin Bunder & Wil Dekkers (1993). Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus. Journal of Symbolic Logic 58 (3):769-788.score: 126.0
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  13. Andreas Knobel (1993). Constructive Set Theoretic Models of Typed Combinatory Logic. Journal of Symbolic Logic 58 (1):99-118.score: 126.0
    We shall present two novel ways of deriving simply typed combinatory models. These are of interest in a constructive setting. First we look at extension models, which are certain subalgebras of full function space models. Then we shall show how the space of singletons of a combinatory model can itself be made into one. The two and the algebras in between will have many common features. We use these two constructions in proving: There is a model of constructive (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  14. Katalin Bimbó (2005). The Church-Rosser Property in Symmetric Combinatory Logic. Journal of Symbolic Logic 70 (2):536 - 556.score: 126.0
    Symmetic 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 combinators 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 (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. Andrea Cantini (2002). Polytime, Combinatory Logic and Positive Safe Induction. Archive for Mathematical Logic 41 (2):169-189.score: 126.0
    We characterize the polynomial time operations as those which are provably total in a first order system, which comprises (untyped) combinatory logic with extensionality, together with positive “safe induction” on the set of binary strings. The formalization of safe induction is inspired by Leivants idea of ramification. We also show how to replace ramification by means of modal logic.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  16. Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of Two Systems of Illative Combinatory Logic for First-Order Propositional and Predicate Calculus. Archive for Mathematical Logic 37 (5-6):327-341.score: 126.0
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  17. Lou Goble (2007). Combinatory Logic and the Semantics of Substructural Logics. Studia Logica 85 (2):171 - 197.score: 120.0
    The results of this paper extend some of the intimate relations that are known to obtain between combinatory logic and certain substructural logics to establish a general characterization theorem that applies to a very broad family of such logics. In particular, I demonstrate that, for every combinator X, if LX is the logic that results by adding the set of types assigned to X (in an appropriate type assignment system, TAS) as axioms to the basic positive relevant (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  18. M. W. Bunder (1988). Arithmetic Based on the Church Numerals in Illative Combinatory Logic. Studia Logica 47 (2):129 - 143.score: 120.0
    In the early thirties, Church developed predicate calculus within a system based on lambda calculus. Rosser and Kleene developed Arithmetic within this system, but using a Godelization technique showed the system to be inconsistent.Alternative systems to that of Church have been developed, but so far more complex definitions of the natural numbers have had to be used. The present paper based on a system of illative combinatory logic developed previously by the author, does allow the use of the (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  19. Jonathan P. Seldin (2000). On the Role of Implication in Formal Logic. Journal of Symbolic Logic 65 (3):1076-1114.score: 114.0
    Evidence is given that implication (and its special case, negation) carry the logical strength of a system of formal logic. This is done by proving normalization and cut elimination for a system based on combinatory logic or λ-calculus with logical constants for and, or, all, and exists, but with none for either implication or negation. The proof is strictly finitary, showing that this system is very weak. The results can be extended to a "classical" version of the (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  20. Pierluigi Minari (2004). Analytic Combinatory Calculi and the Elimination of Transitivity. Archive for Mathematical Logic 43 (2):159-191.score: 114.0
    We introduce, in a general setting, an ‘‘analytic’’ version of standard equational calculi of combinatory logic. Analyticity lies on the one side in the fact that these calculi are characterized by the presence of combinatory introduction rules in place of combinatory axioms, and on the other side in that the transitivity rule proves to be eliminable. Apart from consistency, which follows immediately, we discuss other almost direct consequences of analyticity and the main transitivity elimination theorem; in (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  21. Pierluigi Minari (2009). A Solution to Curry and Hindley's Problem on Combinatory Strong Reduction. Archive for Mathematical Logic 48 (2):159-184.score: 114.0
    It has often been remarked that the metatheory of strong reduction $\succ$ , the combinatory analogue of βη-reduction ${\twoheadrightarrow_{\beta\eta}}$ in λ-calculus, is rather complicated. In particular, although the confluence of $\succ$ is an easy consequence of ${\twoheadrightarrow_{\beta\eta}}$ being confluent, no direct proof of this fact is known. Curry and Hindley’s problem, dating back to 1958, asks for a self-contained proof of the confluence of $\succ$ , one which makes no detour through λ-calculus. We answer positively to this question, by (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  22. William R. Stirton (2012). How to Assign Ordinal Numbers to Combinatory Terms with Polymorphic Types. Archive for Mathematical Logic 51 (5-6):475-501.score: 114.0
    The article investigates a system of polymorphically typed combinatory logic which is equivalent to Gödel’s T. A notion of (strong) reduction is defined over terms of this system and it is proved that the class of well-formed terms is closed under both bracket abstraction and reduction. The main new result is that the number of contractions needed to reduce a term to normal form is computed by an ε 0-recursive function. The ordinal assignments used to obtain this result (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  23. Sabine Broda & Luís Damas (1997). Compact Bracket Abstraction in Combinatory Logic. Journal of Symbolic Logic 62 (3):729-740.score: 110.0
    Translations from Lambda calculi into combinatory logics can be used to avoid some implementational problems of the former systems. However, this scheme can only be efficient if the translation produces short output with a small number of combinators, in order to reduce the time and transient storage space spent during reduction of combinatory terms. In this paper we present a combinatory system and an abstraction algorithm, based on the original bracket abstraction operator of Schonfinkel [9]. The algorithm (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  24. Katalin Bimbó (2003). The Church-Rosser Property in Dual Combinatory Logic. Journal of Symbolic Logic 68 (1):132-152.score: 108.0
    Dual 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 (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  25. Katalin Bimb� (2003). The Church-Rosser Property in Dual Combinatory Logic. Journal of Symbolic Logic 68 (1):132 - 152.score: 108.0
    Dual 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 (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  26. Martin W. Bunder, J. Roger Hindley & Jonathan P. Seldin (1989). On Adding (Ξ) to Weak Equality in Combinatory Logic. Journal of Symbolic Logic 54 (2):590-607.score: 102.0
    Because the main difference between combinatory weak equality and λβ-equality is that the rule \begin{equation*}\tag{\xi} X = Y \vdash \lambda x.X = \lambda x.Y\end{equation*} is valid for the latter but not the former, it is easy to assume that another way of defining combinatory β-equality is to add rule (ξ) to the postulates for weak equality. However, to make this true, one must choose the definition of combinatory abstraction in (ξ) very carefully. If one tries to use (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  27. Haskell B. Curry, J. Roger Hindley & J. P. Seldin (eds.) (1980). To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press.score: 102.0
  28. Raymond M. Smullyan (1985). To Mock a Mocking Bird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic. Knopf.score: 102.0
     
    My bibliography  
     
    Export citation  
  29. S. Kamal Abdali (1976). An Abstraction Algorithm for Combinatory Logic. Journal of Symbolic Logic 41 (1):222-224.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  30. Frederic B. Fitch (1980). A Consistent Combinatory Logic with an Inverse to Equality. Journal of Symbolic Logic 45 (3):529-543.score: 96.0
  31. Nicolas D. Goodman (1972). A Simplification of Combinatory Logic. Journal of Symbolic Logic 37 (2):225-246.score: 96.0
  32. Haskell B. Curry (1941). A Revision of the Fundamental Rules of Combinatory Logic. Journal of Symbolic Logic 6 (2):41-53.score: 96.0
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  33. M. W. Bunder (1974). Various Systems of Set Theory Based on Combinatory Logic. Notre Dame Journal of Formal Logic 15 (2):192-206.score: 96.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  34. M. W. Bunder (1987). Some Consistency Proofs and a Characterization of Inconsistency Proofs in Illative Combinatory Logic. Journal of Symbolic Logic 52 (1):89-110.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  35. John T. Kearns (1969). Combinatory Logic with Discriminators. Journal of Symbolic Logic 34 (4):561-575.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  36. Frederic B. Fitch (1963). The System Cδ of Combinatory Logic. Journal of Symbolic Logic 28 (1):87-97.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  37. M. W. Bunder (1983). A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic. Journal of Symbolic Logic 48 (3):771-776.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  38. Roger Hindley (1967). Axioms for Strong Reduction in Combinatory Logic. Journal of Symbolic Logic 32 (2):224-236.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  39. John T. Kearns (1973). The Completeness of Combinatory Logic with Discriminators. Notre Dame Journal of Formal Logic 14 (3):323-330.score: 96.0
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  40. Luis E. Sanchis (1964). Types in Combinatory Logic. Notre Dame Journal of Formal Logic 5 (3):161-180.score: 96.0
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  41. M. W. Bunder (1982). Illative Combinatory Logic Without Equality as a Primitive Predicate. Notre Dame Journal of Formal Logic 23 (1):62-70.score: 96.0
  42. M. W. Bunder (1977). Consistency Notions in Illative Combinatory Logic. Journal of Symbolic Logic 42 (4):527-529.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  43. Bruce Lercher (1967). Strong Reduction and Normal Form in Combinatory Logic. Journal of Symbolic Logic 32 (2):213-223.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  44. M. W. Bunder (1974). Propositional and Predicate Calculuses Based on Combinatory Logic. Notre Dame Journal of Formal Logic 15 (1):25-34.score: 96.0
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  45. Remi Legrand (1988). A Basis Result in Combinatory Logic. Journal of Symbolic Logic 53 (4):1224-1226.score: 96.0
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  46. M. W. Bunder (1970). A Paradox in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 11 (4):467-470.score: 96.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  47. M. W. Bunder (1979). $\Lambda$-Elimination in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):628-630.score: 96.0
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  48. Patricia Johann (1994). Normal Forms in Combinatory Logic. Notre Dame Journal of Formal Logic 35 (4):573-594.score: 96.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  49. Alberto Pettorossi (1981). A Property Which Guarantees Termination in Weak Combinatory Logic and Subtree Replacement Systems. Notre Dame Journal of Formal Logic 22 (4):344-356.score: 96.0
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  50. Edward J. Cogan (1955). A Formalization of the Theory of Sets From the Point of View of Combinatory Logic. Mathematical Logic Quarterly 1 (3):198-240.score: 96.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 1000