Summary of the monograph on λ-calculus
This text is an extremely concise summary of the classical monograph on the λ-calculus (H. Barendregt, "Lambda-calculus. Its syntax and semantics", translated from English by G. E. Mints, edited by A. Kuzicheva, Moscow, "World" , 1985). It may be of interest to all those who planned to undertake a systematic study of this topic, having familiarized with it in general terms, but postponed due to the complex structure of the main monograph, the definitions and main results in which are rather fragmented. Here we will try to make the presentation, on the contrary, absolutely linear, and, of course, incomparably shorter, avoiding unnecessary definitions and examples, and focusing on the necessary terminology, notation and statements, which, in turn, are set out close to the original text. We begin by defining the system λβη, that is, the classical typeless extensional λ-calculus. Then we proceed to combinatorial logic, the fixed point theorem and syntactic sugar. Finally, the final part of the abstract is the construction of a topology on the expressions of this system, designed to explain the apparent contradiction: the representations of the set of expressions in themselves are contained in the set itself with its countability. In fact, a set is endowed with a proper topology, in which expressions are continuous mappings.
The set of λ- expressions Λ is constructed inductively from variables
x, y, z ... ∈ Λ
')
using abstractions
M ∈ Λ ⇒ λx.M ∈ Λ
and applications
M, N ∈ Λ ⇒ MN ∈ Λ,
while the application is left-associative:
(M) ≣ M, MNP ≣ (MN) P.
The reflexive transitive relation Μ ⊂ N means that M is a subexpression of the expression N:
M ⊂ M ⊂ λx.M;
M ⊂ MN ⊃ N;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.
FV (M) is the set of free variables in the expression M:
FV (x) ≣ {x};
FV (λx.M) ≣ FV (M) ∖ {x};
FV (MN) ≣ FV (M) ∪ FV (N).
Variables that are not free are called bound and can be replaced with another variable (this conversion is called α-conversion):
y ∉ FV (M) ⇒ λx.M ≣ λy.M [x: = y], where M [x: = N] is the result of the substitution :
x [x: = P] ≣ P;
y [x: = P] ≣ y;
(λx.M) [x: = P] ≣ λx.M;
(λy.M) [x: = P] ≣ λy.M [x: = P];
(MN) [x: = P] ≣ M [x: = P] N [x: = P].
In the fourth paragraph, it is not necessary to specifically stipulate the condition "x ≢ y and y FV (P)", since it is fulfilled by virtue of the agreement on variables: if the terms M 1 , ..., M n occur in a specific mathematical context, then it is assumed that related variables in them are chosen so that they are different from the free variables.
If the set FV (M) is empty, then M is called a combinator . The set of all combinators denote Λ 0 :
Λ 0 ≣ {M ∈ Λ | FV (M) = ∅}.
The following ratios β, η, and βη are reductions :
β ≣ {((λx.M) N, M [x: = N]) | M, N ∈ Λ};
η ≣ {(λx.M x, M) | M ∈ Λ, x ∉ FV (M)};
βη ≣ β ∪ η.
The expression whose subexpression is a hole is called a context and is denoted by C [], while C [M] is the result of substituting the expression M instead of a hole in the context of C [].
If σ is a reduction, then the expression M is a σ -redex if ∃N: (M, N) ∈ σ. You can also talk about σ- conversion "= σ ":
(M, N) ∈ σ ⇒ C [Μ] → σ C [N];
M ↠ σ M;
M → σ N ⇒ M ↠ σ N;
M → σ N ∧ N → σ P ⇒ M ↠ σ P;
∃P: M ↠ σ P ∧ N ↠ σ P ⇒ M = σ N.
σ- normal form is the expression Μ, if ∄Ν: M → σ Ν. In the extensional λ-calculus, under a redex mean βη-redex, and under the normal form - βη-normal form. It is said that M has the normal form N, if M ↠ N. Moreover, the βη-conversion is usually denoted simply “=”, and this is not accidental: formally, the system λβη is an equational theory. Since such theories are free from logic, consistency in them is determined somewhat differently.
As equality, we consider a formula of the form M = N, where M, N are λ-expressions; such an equality is closed if M and N are combinators. Let T be a formal theory whose formulas are equalities. Then they say that T is consistent (and they write Con (T)) if not every closed equality is provable in T. Otherwise, it is said that T is inconsistent . One of the reasons for considering λβη is that this theory has a certain property of completeness. An equational theory T is called Hilbert-Post full (abbreviated HP-complete) if for any equality M = N in the language of the theory T or M = N is provable, or T + (M = N) is inconsistent. HP-complete theories correspond to maximal consistent theories in the theory of models for first-order logic.
A strategy is a mapping F: Λ → Λ such that ∀M: M ↠ F (M). For a one-step strategy, ∀M: M → F (M) holds. A strategy is called normalizing if for any expression M having the normal form N, for some number n, F n (M) N. The left reduction F l is one of the simplest one-step normalizing strategies: it consists of choosing β-redex, the icons “Λ” in which it is textually to the left than other β-Redexes, or left η-Redex, if β-Redexes do not exist. Thus, if two terms have a common normal form, then using the left reduction, the proof of the corresponding formula can be obtained in a finite number of simple steps. If the formula is unprovable, then either the process does not end at all, or it ends on different normal forms.
The set of combinators Ξ generates the smallest set Ξ + as a closure by application:
Ξ ⊆ Ξ + ;
M, N ∈ Ξ + ⇒ Μ Ν ∈ Ξ + .
A set is called a basis if ∀M ∈ Λ 0 : ∃N ∈ Ξ + : M = N.
Arbitrary abstraction can be modeled with S and K:
S ≣ λx.λy.λz.xz (yz);
K ≣ λx.λy.x;
I ≣ λx.x = SKK;
x ∉ FV (P) ⇒ λx.P = KP;
λx.PQ = S (λx.P) (λx.Q).
Consequently, the combinators K and S define a basis. An arbitrary combinator M is often described not as a λ-expression, but with the help of axioms. For example, the formal system of combinatorial logic CL is defined by two axioms:
KPQ = P;
SPQR = PR (QR).
There are also one-point bases: one of such bases is set by the combinator
X ≣ λx.x KS K.
Indeed, it is easy to verify that XXX = K and X (XX) = S.
Standard combinators are not only components of some basis for combinatorial logic, but also many other useful λ-expressions. One of the first examples is usually given by the simplest combinator, which has no normal form:
Ω ω ω, where ω λx.x x.
Further, the truth values of T ≣ K and F ≣ λx.I allow us to use the expression BMN for the operation “if B, then M, otherwise, N”. Indeed: if B = T, then the expression is M; if B = F, then the expression is N. If B is different from T and F, then the result can be arbitrary.
As in set theory, ordered pairs can be defined in λ-calculus:
[M, N] ≣ λx.x MN, [M, N] T M, [M, N] F ↠ N.
The digital system is a sequence of combinators ⎡0⎤, ⎡1⎤, ⎡2⎤ ..., for which there is a following S + and a zero check for Zero:
S + ⎡n⎤ = ⎡n + 1⎤;
Zero ⎡0⎤ = T;
Zero ⎡n + 1⎤ = F.
In the standard digital system selected
⎡0⎤ ≣ I;
S + ≣ λx. [F, x];
Zero ≣ λx.x T.
A digital system is called adequate if all recursive functions are definable relative to it. To fulfill this property, it suffices that the preceding function P - be found . For a standard digital system, this is a combinator.
P - ≣ λx.x F.
One of the main results of the λ-calculus is the fixed-point theorem: for any F, there exists X, such that FX = X. Its proof is constructive. Let W ≣ λx.F (xx) and X ≣ W W. Then we have X ≣ (λx.F (xx)) W = F (WW) = FX, as required. The reader may have noticed one feature in the proof of this theorem. To establish that FX = X, we start with the term X and reduce it to FX, and not vice versa.
A fixed point combinator is a term M, such that for any F, MF = F (MF) holds, that is, MF is a fixed point for F. An example of a fixed point combinator is often
Y ≣ λf. (Λx.f (xx)) (λx.f (xx)).
The fixed point combinator allows to solve problems of the following type: to construct F, such that
F xy = F yx F.
Indeed, the solution is simple:
F xy = F yx F follows from the equality F = λx.λy.F yx F,
and it follows from F = (λf.λx.λy.fyxf) F.
Now we put F ≣ Y (λf.λx.λy.fyxf), and everything is in order.
We introduce some notation. First, the metalambda abstraction λ x.f (x) is an unnamed record of the set-theoretic function f, for example ( λ x.x 2 + 1) (3) = 10. Secondly, we define the set of codes of finite sequences (for some standard their coding is natural numbers)
Seq = {<n 1 , ..., n k > | k ∈ N, n 1 , ..., n k ∈ N} ∪ {<>};
lh (<>) = 0;
α = <n 1 , ..., n k > ∈ Seq ⇒ lh (α) = k;
α = <m 1 , ..., m p >, β = <n 1 , ..., n q > ∈ Seq ⇒ a * b = <m 1 , ..., m p , n 1 , ..., n q >;
α = <m 1 , ..., m p >, β = <n 1 , ..., n q > ∈ Seq ∧ p ≤ q ∧ m 1 = n 1 ∧… ∧ m p = n p ⇒ α ≤ β.
Let D = (D, ⊑) be a partially ordered set with a reflexive relation ⊑. Then a subset X ⊆ D is called directional if
X ≠ ∅ ∧ ∀x, y ∈ X: ∃z ∈ X: x ⊑ z ∧ y ⊑ z.
Moreover, D is called complete if for any directed subset X ⊆ D there is a supremum ⊔X ∈ D and there is a bottom :
∃⊥ ∈ D: ∀x ∈ D: ⊥ ⊑ x.
The Scott topology on a complete partially ordered set (D, ⊑) is defined as follows: O ⊆ D is considered open if
1) x ∈ O ∧ x ⊑ y ⇒ y ∈ O;
2) X ⊆ D ∧ ⊔X ∈ O ⇒ X ∩ O ≠ ∅.
A partial mapping φ: X ↝ Y is a mapping φ such that the domain of definition Dom (φ) ⊆ X. For x ∈ X, φ (x) ↓ means that φ (x) is defined, that is, x ∈ Dom (φ ); φ (x) means that φ (x) is not defined, that is, x ∉ Dom (φ).
If Σ is a set of symbols, then a partially Σ-labeled tree is a partial mapping φ: Seq ↝ Σ × N, such that
1) φ (σ) ↓ ∧ τ ≤ σ ⇒ φ (τ) ↓;
2) φ (σ) = <a, n> ⇒ ∀k ≥ n: φ (σ * <k>).
The bare tree underlying the partially Σ-labeled tree φ is a tree
T φ = {<>} ∪ {σ | σ = σ '* <k> ∧ φ (σ') = <a, n> ∧ k <n}.
If σ ∈ T φ and φ (σ) = <a, n>, then a is called a label in the node σ. If for σ ∈ T φ φ (σ) ↑, then we say that the node σ is unlabeled. Partially labeled trees will be denoted by capital letters and we will write σ ∈ A instead of σ ∈ T A and A (α) = ⊥, when A (α) ↑, but still α ∈ A.
If Σ = {λx 1. … Λx n .x | n ≥ 0, x 1 , ..., x n , x ∈ Λ}, then the partially Σ-labeled tree is called a Böhm type tree . We denote the set of all such trees by B. The subtree of tree A, originating from node α, is A α = λ β.A (α * β). Obviously, ∈A ∈ B: ∀α: A α ∈ B.
The combinator M is solvable if
∃n: ∃N 1 , ..., N n ∈ Λ 0 : MN 1 ... N n = I.
For example, a fixed point combinator is solvable, since Y (KI) = KI (Y (KI)) = I. On the other hand, Ω is insoluble. An arbitrary λ-expression is soluble if the combinator λx 1. … Λx n .M is solvable, where {x 1 ,…, x n } = FV (M).
The λ-expression M is a head normal form if it is
M ≣ λx 1. ... λx n .x M 1 ... M m , m, n ≥ 0.
It is said that M has a head normal form N, if M = N. The main one is that head normal form of expression, which is first achieved by its left reduction.
Wadsworth introduced a class of λ-expressions that do not have a head normal form, and argued that the elements of this class should be considered as meaningless expressions in λ-calculus. He also owns the following important result: A λ-expression is solvable if and only if it has a head normal form. Thus, from the insolubility of M it follows that for any expressions N 1 , ..., N n the expression MN 1 ... N n has no normal form.
The Boma tree for the term M, denoted by BT (M), is a Bem tree of type defined as follows:
1) if M is insoluble, then ∀σ: BT (Μ) (σ) ↑,
2) if M is soluble and has the principal head normal form λx 1. ... λx n .x M 0 ... M m - 1 , then
BT (M) (<>) = <λx 1. … Λx n .x, m>;
k <m ⇒ BT (M) (<k> * σ) = BT (M k ) (σ);
k ≥ m ⇒ BT (M) (<k> * σ).
Consider the complete partially ordered set B = (B,) with the Scott topology. The tree topology on the set Λ is the smallest topology in which the mapping BT is continuous: Λ → B. In other words, the open subsets of Λ are BT -1 (O), where O is open in the Scott topology on B.
Using the tree topology, one can express the usual concepts related to λ-calculus in topological terms. For example, normal forms turn out to be isolated points, and unsolvable expressions are compactification points , that is, such points whose only neighborhood is the topological space itself.
It is proved that application and abstraction are continuous in the tree topology on Λ, and for application it is a non-trivial result, which has interesting consequences. For example, the set Sol ⊆ Λ of soluble terms is open. Indeed, in any complete partially ordered set {x | x ≠ ⊥} open to Scott. Therefore, the set Sol = BT -1 {A | A ≠ ⊥} is open in Λ.
Theory
The set of λ- expressions Λ is constructed inductively from variables
x, y, z ... ∈ Λ
')
using abstractions
M ∈ Λ ⇒ λx.M ∈ Λ
and applications
M, N ∈ Λ ⇒ MN ∈ Λ,
while the application is left-associative:
(M) ≣ M, MNP ≣ (MN) P.
The reflexive transitive relation Μ ⊂ N means that M is a subexpression of the expression N:
M ⊂ M ⊂ λx.M;
M ⊂ MN ⊃ N;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.
FV (M) is the set of free variables in the expression M:
FV (x) ≣ {x};
FV (λx.M) ≣ FV (M) ∖ {x};
FV (MN) ≣ FV (M) ∪ FV (N).
Variables that are not free are called bound and can be replaced with another variable (this conversion is called α-conversion):
y ∉ FV (M) ⇒ λx.M ≣ λy.M [x: = y], where M [x: = N] is the result of the substitution :
x [x: = P] ≣ P;
y [x: = P] ≣ y;
(λx.M) [x: = P] ≣ λx.M;
(λy.M) [x: = P] ≣ λy.M [x: = P];
(MN) [x: = P] ≣ M [x: = P] N [x: = P].
In the fourth paragraph, it is not necessary to specifically stipulate the condition "x ≢ y and y FV (P)", since it is fulfilled by virtue of the agreement on variables: if the terms M 1 , ..., M n occur in a specific mathematical context, then it is assumed that related variables in them are chosen so that they are different from the free variables.
If the set FV (M) is empty, then M is called a combinator . The set of all combinators denote Λ 0 :
Λ 0 ≣ {M ∈ Λ | FV (M) = ∅}.
The following ratios β, η, and βη are reductions :
β ≣ {((λx.M) N, M [x: = N]) | M, N ∈ Λ};
η ≣ {(λx.M x, M) | M ∈ Λ, x ∉ FV (M)};
βη ≣ β ∪ η.
The expression whose subexpression is a hole is called a context and is denoted by C [], while C [M] is the result of substituting the expression M instead of a hole in the context of C [].
If σ is a reduction, then the expression M is a σ -redex if ∃N: (M, N) ∈ σ. You can also talk about σ- conversion "= σ ":
(M, N) ∈ σ ⇒ C [Μ] → σ C [N];
M ↠ σ M;
M → σ N ⇒ M ↠ σ N;
M → σ N ∧ N → σ P ⇒ M ↠ σ P;
∃P: M ↠ σ P ∧ N ↠ σ P ⇒ M = σ N.
σ- normal form is the expression Μ, if ∄Ν: M → σ Ν. In the extensional λ-calculus, under a redex mean βη-redex, and under the normal form - βη-normal form. It is said that M has the normal form N, if M ↠ N. Moreover, the βη-conversion is usually denoted simply “=”, and this is not accidental: formally, the system λβη is an equational theory. Since such theories are free from logic, consistency in them is determined somewhat differently.
As equality, we consider a formula of the form M = N, where M, N are λ-expressions; such an equality is closed if M and N are combinators. Let T be a formal theory whose formulas are equalities. Then they say that T is consistent (and they write Con (T)) if not every closed equality is provable in T. Otherwise, it is said that T is inconsistent . One of the reasons for considering λβη is that this theory has a certain property of completeness. An equational theory T is called Hilbert-Post full (abbreviated HP-complete) if for any equality M = N in the language of the theory T or M = N is provable, or T + (M = N) is inconsistent. HP-complete theories correspond to maximal consistent theories in the theory of models for first-order logic.
A strategy is a mapping F: Λ → Λ such that ∀M: M ↠ F (M). For a one-step strategy, ∀M: M → F (M) holds. A strategy is called normalizing if for any expression M having the normal form N, for some number n, F n (M) N. The left reduction F l is one of the simplest one-step normalizing strategies: it consists of choosing β-redex, the icons “Λ” in which it is textually to the left than other β-Redexes, or left η-Redex, if β-Redexes do not exist. Thus, if two terms have a common normal form, then using the left reduction, the proof of the corresponding formula can be obtained in a finite number of simple steps. If the formula is unprovable, then either the process does not end at all, or it ends on different normal forms.
Sugar
The set of combinators Ξ generates the smallest set Ξ + as a closure by application:
Ξ ⊆ Ξ + ;
M, N ∈ Ξ + ⇒ Μ Ν ∈ Ξ + .
A set is called a basis if ∀M ∈ Λ 0 : ∃N ∈ Ξ + : M = N.
Arbitrary abstraction can be modeled with S and K:
S ≣ λx.λy.λz.xz (yz);
K ≣ λx.λy.x;
I ≣ λx.x = SKK;
x ∉ FV (P) ⇒ λx.P = KP;
λx.PQ = S (λx.P) (λx.Q).
Consequently, the combinators K and S define a basis. An arbitrary combinator M is often described not as a λ-expression, but with the help of axioms. For example, the formal system of combinatorial logic CL is defined by two axioms:
KPQ = P;
SPQR = PR (QR).
There are also one-point bases: one of such bases is set by the combinator
X ≣ λx.x KS K.
Indeed, it is easy to verify that XXX = K and X (XX) = S.
Standard combinators are not only components of some basis for combinatorial logic, but also many other useful λ-expressions. One of the first examples is usually given by the simplest combinator, which has no normal form:
Ω ω ω, where ω λx.x x.
Further, the truth values of T ≣ K and F ≣ λx.I allow us to use the expression BMN for the operation “if B, then M, otherwise, N”. Indeed: if B = T, then the expression is M; if B = F, then the expression is N. If B is different from T and F, then the result can be arbitrary.
As in set theory, ordered pairs can be defined in λ-calculus:
[M, N] ≣ λx.x MN, [M, N] T M, [M, N] F ↠ N.
The digital system is a sequence of combinators ⎡0⎤, ⎡1⎤, ⎡2⎤ ..., for which there is a following S + and a zero check for Zero:
S + ⎡n⎤ = ⎡n + 1⎤;
Zero ⎡0⎤ = T;
Zero ⎡n + 1⎤ = F.
In the standard digital system selected
⎡0⎤ ≣ I;
S + ≣ λx. [F, x];
Zero ≣ λx.x T.
A digital system is called adequate if all recursive functions are definable relative to it. To fulfill this property, it suffices that the preceding function P - be found . For a standard digital system, this is a combinator.
P - ≣ λx.x F.
One of the main results of the λ-calculus is the fixed-point theorem: for any F, there exists X, such that FX = X. Its proof is constructive. Let W ≣ λx.F (xx) and X ≣ W W. Then we have X ≣ (λx.F (xx)) W = F (WW) = FX, as required. The reader may have noticed one feature in the proof of this theorem. To establish that FX = X, we start with the term X and reduce it to FX, and not vice versa.
A fixed point combinator is a term M, such that for any F, MF = F (MF) holds, that is, MF is a fixed point for F. An example of a fixed point combinator is often
Y ≣ λf. (Λx.f (xx)) (λx.f (xx)).
The fixed point combinator allows to solve problems of the following type: to construct F, such that
F xy = F yx F.
Indeed, the solution is simple:
F xy = F yx F follows from the equality F = λx.λy.F yx F,
and it follows from F = (λf.λx.λy.fyxf) F.
Now we put F ≣ Y (λf.λx.λy.fyxf), and everything is in order.
Topology
We introduce some notation. First, the metalambda abstraction λ x.f (x) is an unnamed record of the set-theoretic function f, for example ( λ x.x 2 + 1) (3) = 10. Secondly, we define the set of codes of finite sequences (for some standard their coding is natural numbers)
Seq = {<n 1 , ..., n k > | k ∈ N, n 1 , ..., n k ∈ N} ∪ {<>};
lh (<>) = 0;
α = <n 1 , ..., n k > ∈ Seq ⇒ lh (α) = k;
α = <m 1 , ..., m p >, β = <n 1 , ..., n q > ∈ Seq ⇒ a * b = <m 1 , ..., m p , n 1 , ..., n q >;
α = <m 1 , ..., m p >, β = <n 1 , ..., n q > ∈ Seq ∧ p ≤ q ∧ m 1 = n 1 ∧… ∧ m p = n p ⇒ α ≤ β.
Let D = (D, ⊑) be a partially ordered set with a reflexive relation ⊑. Then a subset X ⊆ D is called directional if
X ≠ ∅ ∧ ∀x, y ∈ X: ∃z ∈ X: x ⊑ z ∧ y ⊑ z.
Moreover, D is called complete if for any directed subset X ⊆ D there is a supremum ⊔X ∈ D and there is a bottom :
∃⊥ ∈ D: ∀x ∈ D: ⊥ ⊑ x.
The Scott topology on a complete partially ordered set (D, ⊑) is defined as follows: O ⊆ D is considered open if
1) x ∈ O ∧ x ⊑ y ⇒ y ∈ O;
2) X ⊆ D ∧ ⊔X ∈ O ⇒ X ∩ O ≠ ∅.
A partial mapping φ: X ↝ Y is a mapping φ such that the domain of definition Dom (φ) ⊆ X. For x ∈ X, φ (x) ↓ means that φ (x) is defined, that is, x ∈ Dom (φ ); φ (x) means that φ (x) is not defined, that is, x ∉ Dom (φ).
If Σ is a set of symbols, then a partially Σ-labeled tree is a partial mapping φ: Seq ↝ Σ × N, such that
1) φ (σ) ↓ ∧ τ ≤ σ ⇒ φ (τ) ↓;
2) φ (σ) = <a, n> ⇒ ∀k ≥ n: φ (σ * <k>).
The bare tree underlying the partially Σ-labeled tree φ is a tree
T φ = {<>} ∪ {σ | σ = σ '* <k> ∧ φ (σ') = <a, n> ∧ k <n}.
If σ ∈ T φ and φ (σ) = <a, n>, then a is called a label in the node σ. If for σ ∈ T φ φ (σ) ↑, then we say that the node σ is unlabeled. Partially labeled trees will be denoted by capital letters and we will write σ ∈ A instead of σ ∈ T A and A (α) = ⊥, when A (α) ↑, but still α ∈ A.
If Σ = {λx 1. … Λx n .x | n ≥ 0, x 1 , ..., x n , x ∈ Λ}, then the partially Σ-labeled tree is called a Böhm type tree . We denote the set of all such trees by B. The subtree of tree A, originating from node α, is A α = λ β.A (α * β). Obviously, ∈A ∈ B: ∀α: A α ∈ B.
The combinator M is solvable if
∃n: ∃N 1 , ..., N n ∈ Λ 0 : MN 1 ... N n = I.
For example, a fixed point combinator is solvable, since Y (KI) = KI (Y (KI)) = I. On the other hand, Ω is insoluble. An arbitrary λ-expression is soluble if the combinator λx 1. … Λx n .M is solvable, where {x 1 ,…, x n } = FV (M).
The λ-expression M is a head normal form if it is
M ≣ λx 1. ... λx n .x M 1 ... M m , m, n ≥ 0.
It is said that M has a head normal form N, if M = N. The main one is that head normal form of expression, which is first achieved by its left reduction.
Wadsworth introduced a class of λ-expressions that do not have a head normal form, and argued that the elements of this class should be considered as meaningless expressions in λ-calculus. He also owns the following important result: A λ-expression is solvable if and only if it has a head normal form. Thus, from the insolubility of M it follows that for any expressions N 1 , ..., N n the expression MN 1 ... N n has no normal form.
The Boma tree for the term M, denoted by BT (M), is a Bem tree of type defined as follows:
1) if M is insoluble, then ∀σ: BT (Μ) (σ) ↑,
2) if M is soluble and has the principal head normal form λx 1. ... λx n .x M 0 ... M m - 1 , then
BT (M) (<>) = <λx 1. … Λx n .x, m>;
k <m ⇒ BT (M) (<k> * σ) = BT (M k ) (σ);
k ≥ m ⇒ BT (M) (<k> * σ).
Consider the complete partially ordered set B = (B,) with the Scott topology. The tree topology on the set Λ is the smallest topology in which the mapping BT is continuous: Λ → B. In other words, the open subsets of Λ are BT -1 (O), where O is open in the Scott topology on B.
Using the tree topology, one can express the usual concepts related to λ-calculus in topological terms. For example, normal forms turn out to be isolated points, and unsolvable expressions are compactification points , that is, such points whose only neighborhood is the topological space itself.
It is proved that application and abstraction are continuous in the tree topology on Λ, and for application it is a non-trivial result, which has interesting consequences. For example, the set Sol ⊆ Λ of soluble terms is open. Indeed, in any complete partially ordered set {x | x ≠ ⊥} open to Scott. Therefore, the set Sol = BT -1 {A | A ≠ ⊥} is open in Λ.
Source: https://habr.com/ru/post/141104/
All Articles