Theoretical Pearls: Self-interpretation in lambda calculus

1991 ◽  
Vol 1 (2) ◽  
pp. 229-233 ◽  
Author(s):  
Henk Barendregt
Keyword(s):  
Normal Form ◽  
Programming Languages ◽  
Lambda Calculus ◽  
Direct Consequence ◽  
Functional Program ◽  
Computer Scientists ◽  
Strange Loop ◽  
Reduction Machine ◽  
Image Position ◽  
Computable Functions

Programming languages which are capable of interpreting themselves have been fascinating computer scientists. Indeed, if this is possible then a ‘strange loop’ (in the sense of Hofstadter, 1979) is involved. Nevertheless, the phenomenon is a direct consequence of the existence of universal languages. Indeed, if all computable functions can be captured by a language, then so can the particular job of interpreting the code of a program of that language. Self-interpretation will be shown here to be possible in lambda calculus.The set of λ-terms, notation Λ, is defined by the following abstract syntaxwhereis the set {v, v′, v″, v′″,…} of variables. Arbitrary variables are usually denoted by x, y,z,… and λ-terms by M,N,L,…. A redex is a λ-term of the formthat is, the result of substituting N for (the free occurrences of) x in M. Stylistically, it can be said that λ-terms represent functional programs including their input. A reduction machine executes such terms by trying to reduce them to normal form; that is, redexes are continuously replaced by their contracta until hopefully no more redexes are present. If such a normal form can be reached, then this is the output of the functional program; otherwise, the program diverges.

Theoretical Pearls:Representing ‘undefined’ in lambda calculus

1992 ◽  
Vol 2 (3) ◽  
pp. 367-374 ◽  
Author(s):  
Henk Barendregt
Keyword(s):  
Normal Form ◽  
Recursive Function ◽  
Lambda Calculus ◽  
Recursion Theory ◽  
Partial Recursive Function ◽  
Normalization Theorem ◽  
Image Position

AbstractLet ψ be a partial recursive function (of one argument) with λ-defining termF∈Λ°. This meansThere are several proposals for whatF⌜n⌝ should be in case ψ(n) is undefined: (1) a term without a normal form (Church); (2) an unsolvable term (Barendregt); (3) an easy term (Visser); (4) a term of order 0 (Statman).These four possibilities will be covered by one ‘master’ result of Statman which is based on the ‘Anti Diagonal Normalization Theorem’ of Visser (1980). That ingenious theorem about precomplete numerations of Ershov is a powerful tool with applications in recursion theory, metamathematics of arithmetic and lambda calculus.

scholarly journals The Limits of Computation

Axiomathes ◽  
2021 ◽  
Author(s):  
Andrew Powell
Keyword(s):  
Natural Number ◽  
Set Theory ◽  
Lambda Calculus ◽  
Second Order ◽  
Functional Interpretation ◽  
Arbitrary Type ◽  
Computable Functions

AbstractThis article provides a survey of key papers that characterise computable functions, but also provides some novel insights as follows. It is argued that the power of algorithms is at least as strong as functions that can be proved to be totally computable in type-theoretic translations of subsystems of second-order Zermelo Fraenkel set theory. Moreover, it is claimed that typed systems of the lambda calculus give rise naturally to a functional interpretation of rich systems of types and to a hierarchy of ordinal recursive functionals of arbitrary type that can be reduced by substitution to natural number functions.

Refinements of Vaught's normal from theorem

1979 ◽  
Vol 44 (3) ◽  
pp. 289-306 ◽  
Author(s):  
Victor Harnik
Keyword(s):  
Normal Form ◽  
Boolean Combination ◽  
Form Theorem ◽  
Central Notion ◽  
The Matrix ◽  
Normal Form Theorem ◽  
Skolem Theorem ◽  
Image Position ◽  
Countable Models

The central notion of this paper is that of a (conjunctive) game-sentence, i.e., a sentence of the formwhere the indices ki, ji range over given countable sets and the matrix conjuncts are, say, open -formulas. Such game sentences were first considered, independently, by Svenonius [19], Moschovakis [13]—[15] and Vaught [20]. Other references are [1], [3]—[5], [10]—[12]. The following normal form theorem was proved by Vaught (and, in less general forms, by his predecessors).Theorem 0.1. Let L = L0(R). For every -sentence ϕ there is an L0-game sentence Θ such that ⊨′ ∃Rϕ ↔ Θ.(A word about the notations: L0(R) denotes the language obtained from L0 by adding to it the sequence R of logical symbols which do not belong to L0; “⊨′α” means that α is true in all countable models.)0.1 can be restated as follows.Theorem 0.1′. For every-sentence ϕ there is an L0-game sentence Θ such that ⊨ϕ → Θ and for any-sentence ϕ if ⊨ϕ → ϕ and L′ ⋂ L ⊆ L0, then ⊨ Θ → ϕ.(We sketch the proof of the equivalence between 0.1 and 0.1′.0.1 implies 0.1′. This is obvious once we realize that game sentences and their negations satisfy the downward Löwenheim-Skolem theorem and hence, ⊨′α is equivalent to ⊨α whenever α is a boolean combination of and game sentences.

scholarly journals A combinatory account of internal structure

2011 ◽  
Vol 76 (3) ◽  
pp. 807-826 ◽  
Author(s):  
Barry Jay ◽  
Thomas Given-Wilson
Keyword(s):  
Normal Form ◽  
Internal Structure ◽  
Pattern Matching ◽  
Normal Forms ◽  
Expressive Power ◽  
Combinatory Logic ◽  
Natural Numbers ◽  
Type Information ◽  
Computable Functions

AbstractTraditional combinatory logic uses combinators S and K to represent all Turing-computable functions on natural numbers, but there are Turing-computable functions on the combinators themselves that cannot be so represented, because they access internal structure in ways that S and K cannot. Much of this expressive power is captured by adding a factorisation combinator F. The resulting SF-calculus is structure complete, in that it supports all pattern-matching functions whose patterns are in normal form, including a function that decides structural equality of arbitrary normal forms. A general characterisation of the structure complete, confluent combinatory calculi is given along with some examples. These are able to represent all their Turing-computable functions whose domain is limited to normal forms. The combinator F can be typed using an existential type to represent internal type information.

Using Game Frameworks to Teach Computer Programming

2017 ◽  
pp. 221-236
Author(s):  
Alberto Simões
Keyword(s):  
Programming Languages ◽  
Computer Games ◽  
Computer Programming ◽  
Object Oriented Programming ◽  
Multidimensional Arrays ◽  
Computer Scientists ◽  
Common Framework ◽  
The Common ◽  
Algebraic Operations ◽  
Art Game

Teaching computer programming is an important task in the formation of computer scientists. Being a subject taught in the first years of student degrees, need to properly motivate students, so they try, at home, to learn by themselves, complementing that way their classes. This chapter proposes an approach to computer programming teaching based on the construction of videogames, using state of the art game frameworks. The author will show how the task of writing a game using a common framework deals with the basic programming concepts that are usually taught on a first course on computer programming, namely on object oriented programming languages like C# or Java: algebraic operations with variables, methods declaration, objects definition, objects hierarchy and multidimensional arrays. As it will be shown, even the common order of concepts presentation during the course can be kept, although applying them to computer games instead of the usually requested exercises.

Equational Logic Programming

1998 ◽  
Author(s):  
Michael J. O’Donnell
Keyword(s):  
Normal Form ◽  
Logic Programming ◽  
Programming Languages ◽  
Question Answering ◽  
Normal Forms ◽  
Equational Logic ◽  
Consequence Relation ◽  
Logic Programming Languages ◽  
Semantic Consequence

Sections 2.3.4 and 2.3.5 of the chapter ‘Introduction: Logic and Logic Programming Languages’ are crucial prerequisites to this chapter. I summarize their relevance below, but do not repeat their content. Logic programming languages in general are those that compute by deriving semantic consequences of given formulae in order to answer questions. In equational logic programming languages, the formulae are all equations expressing postulated properties of certain functions, and the questions ask for equivalent normal forms for given terms. Section 2.3.4 of the ‘Introduction . . .’ chapter gives definitions of the models of equational logic, the semantic consequence relation . . . T |=≐(t1 ≐ t2) . . . (t1 ≐ t2 is a semantic consequence of the set T of equations, see Definition 2.3.14), and the question answering relation . . . (norm t1,…,ti : t) ?- ≐ (t ≐ s) . . . (t ≐ s asserts the equality of t to the normal form s, which contains no instances of t1, . . . , ti, see Definition 2.3.16).

Introduction: Logic and Logic Programming Languages

1998 ◽  
Author(s):  
Michael J. O’Donnell
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Historical Development ◽  
Theoretical Computer Science ◽  
Equational Logic ◽  
Computer Scientists ◽  
General Schema ◽  
Similarities And Differences ◽  
Logic Programming Languages ◽  
Order Predicate Calculus

Logic, according to Webster’s dictionary [Webster, 1987], is ‘a science that deals with the principles and criteria of validity of inference and demonstration: the science of the formal principles of reasoning.' Such 'principles and criteria’ are always described in terms of a language in which inference, demonstration, and reasoning may be expressed. One of the most useful accomplishments of logic for mathematics is the design of a particular formal language, the First Order Predicate Calculus (FOPC). FOPC is so successful at expressing the assertions arising in mathematical discourse that mathematicians and computer scientists often identify logic with classical logic expressed in FOPC. In order to explore a range of possible uses of logic in the design of programming languages, we discard the conventional identification of logic with FOPC, and formalize a general schema for a variety of logical systems, based on the dictionary meaning of the word. Then, we show how logic programming languages may be designed systematically for any sufficiently effective logic, and explain how to view Prolog, Datalog, λProlog, Equational Logic Programming, and similar programming languages, as instances of the general schema of logic programming. Other generalizations of logic programming have been proposed independently by Meseguer [Meseguer, 1989], Miller, Nadathur, Pfenning and Scedrov [Miller et al., 1991], Goguen and Burstall [Goguen and Burstall, 1992]. The purpose of this chapter is to introduce a set of basic concepts for understanding logic programming, not in terms of its historical development, but in a systematic way based on retrospective insights. In order to achieve a systematic treatment, we need to review a number of elementary definitions from logic and theoretical computer science and adapt them to the needs of logic programming. The result is a slightly modified logical notation, which should be recognizable to those who know the traditional notation. Conventional logical notation is also extended to new and analogous concepts, designed to make the similarities and differences between logical relations and computational relations as transparent as possible. Computational notation is revised radically to make it look similar to logical notation.

On a Normal Form of the Orthogonal Transformation III

1958 ◽  
Vol 1 (3) ◽  
pp. 183-191 ◽  
Author(s):  
Hans Zassenhaus
Keyword(s):  
Normal Form ◽  
Linear Space ◽  
Bilinear Form ◽  
Matrix Equation ◽  
Orthogonal Transformation ◽  
The Matrix ◽  
Image Position

Under the assumptions of case of theorem 1 we derive from (3.32) the matrix equationso that there corresponds the matrix B to the bilinear form4.1on the linear space4.2and fP,μ, is symmetric if ɛ = (-1)μ+1, anti-symmetric if ɛ = (-1)μ.The last statement remains true in the case a) if P is symmetric irreducible because in that case fP,μ is 0.

Sign in / Sign up

Export Citation Format

Share Document