Abstract of a monograph on the λ-calculus
This text represents a very concise synopsis of the classic monograph on the λ-calculus (Barendregt H., "the lambda-calculus. Its syntax and semantics", translation from English by G. E. mints, edited by S. A. Kuzicheva, Moscow, "Mir", 1985). It may be of interest to all those who planned to undertake a systematic study of this topic, in General, after reading it, but was postponed due to the complicated structure of the main monographs, definitions and basic results which are quite scattered. Here we will try to make a statement, on the contrary, absolutely linear, and certainly far shorter, avoiding the use of unnecessary definitions and examples, focusing on the essential terminology, notation, and statements, which, in turn, is contained close to the original text. We start from the definition of the system λβη, the classic estipulado extensional λ-calculus. Then move on to combinatorial logic, a fixed point theorem and syntactic sugar. Finally, the concluding part of the abstract — the construction of a topology on terms of this system, which is designed to explain the apparent contradiction: display a variety of expressions in themselves is contained in this set with its countability. In fact, many endowed with the proper topology where expression is a continuous mapping.
The set λ-expression Λ is constructed inductively from variable
x, y, z... ∈ Λ
with the help of abstraction
M ∈ Λ ⇒ λx.M ∈ Λ
and applications
M, N ∈ Λ ⇒ M N ∈ Λ,
the application is left-associative:
(M) ≣ M, M N P ≣ (M N) P.
Reflexive transitive relation Μ ⊂ N means that M is a subexpression of the expression N:
M ⊂ M ⊂ λx.M;
M ⊂ M N ⊃ N;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.
FV(M) is the set available variables in the expression M:
FV(x) ≣ {x};
FV(λx.M) ≣ FV(M) ∖ {x};
FV(M N) ≣ FV(M) ∪ FV(N).
Variables that are not free are called connected and can be replaced with another variable (this transformation is called α-conversion):
y ∉ FV(M) ⇒ λx.M ≣ λy.M[x := y], where M[x := N] is the result of a substitution:
x[x := P] ≣ P;
y[x := P] ≣ y;
(λx.M)[x := P] ≣ λx.M;
(λy.M)[x := P] ≣ λy.M[x := P];
(M N)[x := P] ≣ M[x := P] N[x := P].
In the fourth paragraph you do not need to specify the condition "x ≢ y and y ∉ FV(P)" because it is executed in force of the agreement on variables: if in a certain mathematical context meet baths M1,..., Mn, it is assumed that bound variables in them are selected so that they were distinct from free variables.
If the set FV(M) is empty, then M is called a schemer. The set of all combinators denote Λ0:
Λ0 ≣ {M ∈ Λ | FV(M) = ∅}.
The following relations β, η, and βη are reductions:
β ≣ {((λx.M) N, M[x := N]) | M, N ∈ Λ};
η ≣ {(λx.M x, M) | M ∈ Λ, x ∉ FV(M)};
βη ≣ β ∪ η.
Expression subexpression which is a hole, called the context and is denoted by C[ ], while C[M] is the result of the lookup expression M is the hole in the context C[ ].
If σ is reduced, then the expression M — σ-redeks if ∃N: (M, N) ∈ σ. You can also speak of σ-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 called the expression Μ if ∄Ν: M →σ Ν. In the extensional λ-calculus under redeks mean βη-redeks, and under normal form — βη-normal form. Say that M is normal form N if M ↠ N. At the same βη-conversion is commonly referred to just "=", and this is no coincidence: the formal system λβη is the equational theory. Since such theories are free from the logic, the consistency in them is somewhat different.
The equation we'll consider a formula of the form M = N where M, N be λ-expressions; such equality is closed, if M and N are combinators. Let T be a formal theory with formulas of which are equality. Then say that T consistent (and we write Con(T)) if T not closed any provable equality. Otherwise, say T contradictory. One of the reasons for the consideration of the λβη is that this theory has a certain property of completeness. Equational theory T is called complete Hilbert-Post (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) inconsistent. HP-complete theory correspond to the maximal consistent theories in the theory of models for first-order logic.
Strategy is a map F: Λ → Λ, ∀M: M ↠ F(M). A single-step strategy is executed ∀M: M → F(M). Strategy is called normalizing, if for any expression M has normal form N, for some number n running Fn(M) ≣ N. Left reduction Fl is one of the simplest one-step normalizing strategies: the aim is to select β-redeks icon "λ" which is textually to the left than other β-redexes, either left η-redeks if β redexes no. Thus, if two terms have a common normal form, then using the left reduction of the proof of the corresponding formulas can be obtained for a finite number of simple steps. If a formula is unprovable, then either the process is not completed at all, or he is terminated at different normal forms.
Many combinators Ξ generates a minimal set Ξ+ as the circuit in an application:
Ξ ⊆ Ξ+;
M, N ∈ Ξ+ ⇒ Μ Ν ∈ Ξ+.
A lot of Ξ is called basis, if ∀M ∈ Λ0: ∃N ∈ Ξ+: M = N.
Arbitrary abstraction can be modeled using S and K:
S ≣ λx.λy.λz.x z (y z);
K ≣ λx.λy.x;
I ≣ λx.x = S K K;
x ∉ FV(P) ⇒ λx.P = K P;
λx.P Q = S (λx.P) (λx.Q).
Consequently, the combinators K and S set the basis. Arbitrary Combinator M is often described not in the form of λ-expressions and using the axioms. For example, a formal system of combinatorial logic CL is defined by two axioms:
K P Q = P;
S P Q R = P R (Q R).
There are one-point bases: one of these bases sets Combinator
X ≣ λx.x K S K.
Indeed, it is easy to check that X X X = K and X (X X) = S.
Standard combinators are not only components of some basis for combinatory logic, but many other useful λ-expressions. One of the first examples usually give the simplest Combinator, has no normal form:
Ω ≣ ω ω, where ω ≣ λx.x x.
Further, the truth-values T ≣ K and F ≣ λx.I allow you to designate by the expression B M N operation "if B, then M, otherwise N". Indeed, if B = T, then the expression is equal to M; if B = F, then the expression is equal to N. If B is different from T and F, the result can be arbitrary.
As in set theory, λ-calculus it is possible to define ordered pairs:
[M, N] ≣ λx.x M N, [M, N] T ↠ M, [M, N] F ↠ N.
Digital system is the sequence Combinator ⎡0⎤, ⎡1⎤, ⎡2⎤..., for which there are adherence S+ and testing for null Zero:
S+ ⎡n⎤ = ⎡n + 1⎤;
Zero ⎡0⎤ = T;
Zero ⎡n + 1⎤ = F.
In standard the chosen
⎡0⎤ ≣ I;
S+ ≣ λx.[F, x];
Zero ≣ λx.x T.
A digital system is called adequate, if is definable relative to it are all recursive functions. To complete this property, it is sufficient that there be precedence P-. For a standard digital system is a Combinator
P- ≣ λx.F. x
One of the main results of λ-calculus is the fixed point theorem: for any F there is X such that F X = X. the proof constructively. Let W ≣ λx.F (x x) and X ≣ W W. Then we have X ≣ (λx.F (x x)) W = F (W W) = F X, as required. The reader may have noticed one feature in the proof of this theorem. To establish that F X = X, we start with the term X and reducyruet it to F X, and not Vice versa.
fixed point Combinator is a term M such that for any F occurs M F = F (M F), that is, M F is a fixed point for F. as an Example of a fixed point Combinator is often used as
Y ≣ λf.(λx.f (x x)) (λx.f (x x)).
The fixed point Combinator allows to solve problems of the following type: to construct F, such that
F x y = F y x F.
Indeed, the solution is simple:
F x y = F y x F follows from the equality F = λx.λy.F y x F,
and it follows from F = (λf.λx.λy.f y x f) F.
Now put F ≣ Y (λf.λx.λy.f y x f), and everything is in order.
We introduce some notation. First, metaland-abstraction λx.f(x) — nameless record is set-theoretic function f, for example (λx.x2 + 1)(3) = 10. Second, define multiple codes of finite sequences (with any of their standard encoding of natural numbers)
Seq = {<n1,..., nk> | k ∈ N, N1,..., nk ∈ N} ∪ {< >};
lh(< >) = 0;
α = <n1,..., nk> ∈ Seq ⇒ lh(α) = k;
α = <m1,..., mp>, b = <n1,..., nq> ∈ Seq ⇒ a * b = <m1,..., mp, n1,..., nq>;
α = <m1,..., mp>, b = <n1,..., nq> ∈ Seq ∧ p ≤ q ∧ m1 = n1 ∧ ... ∧ mp = np ⇒ α ≤ β.
Let D = (D, ⊑) is a partially ordered set with a reflexive relation ⊑. Then a subset X ⊆ D is called directed if
X ≠ ∅ ∧ ∀x, y ∈ X: ∃z ∈ X: X ⊑ z ∧ y ⊑ z.
In this case D is called complete, if for any directed subset X ⊆ D is supremum ⊔X ∈ D and a bottom ⊥
∃⊥ ∈ D: ∀x ∈ D: ⊥ ⊑ x.
Topology Scott on the complete poset (D, ⊑) is defined as follows: a set O ⊆ D is considered to be open if
1) x ∈ O ∧ x ⊑ y ⇒ y ∈ O;
2) X ⊆ D ∧ ⊔X ∈ O ⇒ X ∩ O ≠ ∅.
Partial mapping φ: X ↝ Y is a mapping φ, such that the domain Dom(φ) ⊆ X. For x ∈ X write φ(x)↓ means that φ(x) is defined, that is, x ∈ Dom(φ); φ(x)↑ means that φ(x) is not defined, that is, x ∉ Dom(φ).
If Σ is some set of characters, then partial Σ-labeled tree is a partial mapping φ: Seq ↝ Σ × N such that
1) φ(σ)↓ ∧ τ ≤ σ ⇒ φ(τ)↓;
2) φ(σ) = <a, n> ⇒ ∀k ≥ n: φ(σ * <k>)↑.
the Naked tree underlying partial Σ-labeled tree φ is a tree
Tφ = {< >} ∪ {σ | σ = σ' * <k> ∧ φ(σ') = <a, n> ∧ k < n}.
If σ ∈ Tφ and φ(σ) = <a, n>, called a label node σ. If σ ∈ Tφ φ(σ)↑, we say that a node σ untagged. Partially labeled trees will be denoted by capital letters and we will write σ ∈ A is σ ∈ TA and A(α) = ⊥, when A(α)↑, but α ∈ A.
If Σ = {λx1....λxn.x | n ≥ 0, x1,..., xn, x ∈ Λ}, then a partially Σ-labeled tree is called tree Belovskogo type. The set of all such up trees denote B. a Subtree of A tree emanating from a node α is Aα = λβ.A(α * β). It is obvious that ∀A ∈ B: ∀α: Aα ∈ B.
Strategist M solvable if
∃n: ∃N1,..., Nn ∈ Λ0: M N1 ... Nn = I.
For example, the fixed point Combinator is solvable, since Y (K I) = K I (Y (K I)) = I. on the other hand, Ω is unsolvable. An arbitrary λ-expression solvable when we allow Combinator λx1....λxn.M, where {x1,..., xn} = FV(M).
λ-expression M is a head normal form if it is
M ≣ λx1....λxn.x M1 Mm, m, n ≥ 0.
Say that M is head normal form N if M = N. Main is called the head normal form of expression, which is achieved first by left reduction.
Wadsworth introduced the class of λ-expressions that do not have a head normal form, and argued in favor of the fact that the members of this class should be seen as meaningless expressions in λ-calculus. He also belongs to the following important result: λ-expression is solvable if and only if it has a head normal form. Thus, insolubility of M it follows that for any expressions N1,..., Nn expression M N1 ... Nn has no normal form.
the Tree of Bema for the term M, denoted using BT(M) is a tree Belovskogo types are defined as follows:
1) if M is unsolvable, then ∀σ: BT(Μ)(σ)↑,
2) if M is solvable and has a principal head normal form λx1....λxn.x M0 Mm — 1,
BT(M)(< >) = <λx1....λxn.x m>;
k < m ⇒ BT(M)(<k> * σ) = BT(Mk)(σ);
k ≥ m ⇒ BT(M)(<k> * σ)↑.
Consider a complete partially ordered set B = (B, ⊆) with the Scott topology. Topology of the trees on the set of Λ is the smallest topology in which continuously displays BT: Λ → B. in Other words, open subsets of Λ have the form BT-1(O), where O is open in the Scott topology on B.
Using the topology tree, one can Express the usual notions related to λ-calculus in topological terms. For example, the normal forms are isolated points, and insoluble expression — points compactification, that is, those points, the only neighborhood which is itself a topological space.
It is proved that the application and abstraction of continuous in the topology of the trees on Λ, and for an application is a nontrivial result that has interesting consequences. For example, the set Sol ⊆ Λ-solvable terms is open. Indeed, in any complete poset the set {x | x ≠ ⊥} is open on Scott. Consequently, many Sol = BT-1{A | A ≠ ⊥} is open in Λ.
Article based on information from habrahabr.ru
Theory
The set λ-expression Λ is constructed inductively from variable
x, y, z... ∈ Λ
with the help of abstraction
M ∈ Λ ⇒ λx.M ∈ Λ
and applications
M, N ∈ Λ ⇒ M N ∈ Λ,
the application is left-associative:
(M) ≣ M, M N P ≣ (M N) P.
Reflexive transitive relation Μ ⊂ N means that M is a subexpression of the expression N:
M ⊂ M ⊂ λx.M;
M ⊂ M N ⊃ N;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.
FV(M) is the set available variables in the expression M:
FV(x) ≣ {x};
FV(λx.M) ≣ FV(M) ∖ {x};
FV(M N) ≣ FV(M) ∪ FV(N).
Variables that are not free are called connected and can be replaced with another variable (this transformation is called α-conversion):
y ∉ FV(M) ⇒ λx.M ≣ λy.M[x := y], where M[x := N] is the result of a substitution:
x[x := P] ≣ P;
y[x := P] ≣ y;
(λx.M)[x := P] ≣ λx.M;
(λy.M)[x := P] ≣ λy.M[x := P];
(M N)[x := P] ≣ M[x := P] N[x := P].
In the fourth paragraph you do not need to specify the condition "x ≢ y and y ∉ FV(P)" because it is executed in force of the agreement on variables: if in a certain mathematical context meet baths M1,..., Mn, it is assumed that bound variables in them are selected so that they were distinct from free variables.
If the set FV(M) is empty, then M is called a schemer. The set of all combinators denote Λ0:
Λ0 ≣ {M ∈ Λ | FV(M) = ∅}.
The following relations β, η, and βη are reductions:
β ≣ {((λx.M) N, M[x := N]) | M, N ∈ Λ};
η ≣ {(λx.M x, M) | M ∈ Λ, x ∉ FV(M)};
βη ≣ β ∪ η.
Expression subexpression which is a hole, called the context and is denoted by C[ ], while C[M] is the result of the lookup expression M is the hole in the context C[ ].
If σ is reduced, then the expression M — σ-redeks if ∃N: (M, N) ∈ σ. You can also speak of σ-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 called the expression Μ if ∄Ν: M →σ Ν. In the extensional λ-calculus under redeks mean βη-redeks, and under normal form — βη-normal form. Say that M is normal form N if M ↠ N. At the same βη-conversion is commonly referred to just "=", and this is no coincidence: the formal system λβη is the equational theory. Since such theories are free from the logic, the consistency in them is somewhat different.
The equation we'll consider a formula of the form M = N where M, N be λ-expressions; such equality is closed, if M and N are combinators. Let T be a formal theory with formulas of which are equality. Then say that T consistent (and we write Con(T)) if T not closed any provable equality. Otherwise, say T contradictory. One of the reasons for the consideration of the λβη is that this theory has a certain property of completeness. Equational theory T is called complete Hilbert-Post (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) inconsistent. HP-complete theory correspond to the maximal consistent theories in the theory of models for first-order logic.
Strategy is a map F: Λ → Λ, ∀M: M ↠ F(M). A single-step strategy is executed ∀M: M → F(M). Strategy is called normalizing, if for any expression M has normal form N, for some number n running Fn(M) ≣ N. Left reduction Fl is one of the simplest one-step normalizing strategies: the aim is to select β-redeks icon "λ" which is textually to the left than other β-redexes, either left η-redeks if β redexes no. Thus, if two terms have a common normal form, then using the left reduction of the proof of the corresponding formulas can be obtained for a finite number of simple steps. If a formula is unprovable, then either the process is not completed at all, or he is terminated at different normal forms.
Sugar
Many combinators Ξ generates a minimal set Ξ+ as the circuit in an application:
Ξ ⊆ Ξ+;
M, N ∈ Ξ+ ⇒ Μ Ν ∈ Ξ+.
A lot of Ξ is called basis, if ∀M ∈ Λ0: ∃N ∈ Ξ+: M = N.
Arbitrary abstraction can be modeled using S and K:
S ≣ λx.λy.λz.x z (y z);
K ≣ λx.λy.x;
I ≣ λx.x = S K K;
x ∉ FV(P) ⇒ λx.P = K P;
λx.P Q = S (λx.P) (λx.Q).
Consequently, the combinators K and S set the basis. Arbitrary Combinator M is often described not in the form of λ-expressions and using the axioms. For example, a formal system of combinatorial logic CL is defined by two axioms:
K P Q = P;
S P Q R = P R (Q R).
There are one-point bases: one of these bases sets Combinator
X ≣ λx.x K S K.
Indeed, it is easy to check that X X X = K and X (X X) = S.
Standard combinators are not only components of some basis for combinatory logic, but many other useful λ-expressions. One of the first examples usually give the simplest Combinator, has no normal form:
Ω ≣ ω ω, where ω ≣ λx.x x.
Further, the truth-values T ≣ K and F ≣ λx.I allow you to designate by the expression B M N operation "if B, then M, otherwise N". Indeed, if B = T, then the expression is equal to M; if B = F, then the expression is equal to N. If B is different from T and F, the result can be arbitrary.
As in set theory, λ-calculus it is possible to define ordered pairs:
[M, N] ≣ λx.x M N, [M, N] T ↠ M, [M, N] F ↠ N.
Digital system is the sequence Combinator ⎡0⎤, ⎡1⎤, ⎡2⎤..., for which there are adherence S+ and testing for null Zero:
S+ ⎡n⎤ = ⎡n + 1⎤;
Zero ⎡0⎤ = T;
Zero ⎡n + 1⎤ = F.
In standard the chosen
⎡0⎤ ≣ I;
S+ ≣ λx.[F, x];
Zero ≣ λx.x T.
A digital system is called adequate, if is definable relative to it are all recursive functions. To complete this property, it is sufficient that there be precedence P-. For a standard digital system is a Combinator
P- ≣ λx.F. x
One of the main results of λ-calculus is the fixed point theorem: for any F there is X such that F X = X. the proof constructively. Let W ≣ λx.F (x x) and X ≣ W W. Then we have X ≣ (λx.F (x x)) W = F (W W) = F X, as required. The reader may have noticed one feature in the proof of this theorem. To establish that F X = X, we start with the term X and reducyruet it to F X, and not Vice versa.
fixed point Combinator is a term M such that for any F occurs M F = F (M F), that is, M F is a fixed point for F. as an Example of a fixed point Combinator is often used as
Y ≣ λf.(λx.f (x x)) (λx.f (x x)).
The fixed point Combinator allows to solve problems of the following type: to construct F, such that
F x y = F y x F.
Indeed, the solution is simple:
F x y = F y x F follows from the equality F = λx.λy.F y x F,
and it follows from F = (λf.λx.λy.f y x f) F.
Now put F ≣ Y (λf.λx.λy.f y x f), and everything is in order.
Topology
We introduce some notation. First, metaland-abstraction λx.f(x) — nameless record is set-theoretic function f, for example (λx.x2 + 1)(3) = 10. Second, define multiple codes of finite sequences (with any of their standard encoding of natural numbers)
Seq = {<n1,..., nk> | k ∈ N, N1,..., nk ∈ N} ∪ {< >};
lh(< >) = 0;
α = <n1,..., nk> ∈ Seq ⇒ lh(α) = k;
α = <m1,..., mp>, b = <n1,..., nq> ∈ Seq ⇒ a * b = <m1,..., mp, n1,..., nq>;
α = <m1,..., mp>, b = <n1,..., nq> ∈ Seq ∧ p ≤ q ∧ m1 = n1 ∧ ... ∧ mp = np ⇒ α ≤ β.
Let D = (D, ⊑) is a partially ordered set with a reflexive relation ⊑. Then a subset X ⊆ D is called directed if
X ≠ ∅ ∧ ∀x, y ∈ X: ∃z ∈ X: X ⊑ z ∧ y ⊑ z.
In this case D is called complete, if for any directed subset X ⊆ D is supremum ⊔X ∈ D and a bottom ⊥
∃⊥ ∈ D: ∀x ∈ D: ⊥ ⊑ x.
Topology Scott on the complete poset (D, ⊑) is defined as follows: a set O ⊆ D is considered to be open if
1) x ∈ O ∧ x ⊑ y ⇒ y ∈ O;
2) X ⊆ D ∧ ⊔X ∈ O ⇒ X ∩ O ≠ ∅.
Partial mapping φ: X ↝ Y is a mapping φ, such that the domain Dom(φ) ⊆ X. For x ∈ X write φ(x)↓ means that φ(x) is defined, that is, x ∈ Dom(φ); φ(x)↑ means that φ(x) is not defined, that is, x ∉ Dom(φ).
If Σ is some set of characters, then partial Σ-labeled tree is a partial mapping φ: Seq ↝ Σ × N such that
1) φ(σ)↓ ∧ τ ≤ σ ⇒ φ(τ)↓;
2) φ(σ) = <a, n> ⇒ ∀k ≥ n: φ(σ * <k>)↑.
the Naked tree underlying partial Σ-labeled tree φ is a tree
Tφ = {< >} ∪ {σ | σ = σ' * <k> ∧ φ(σ') = <a, n> ∧ k < n}.
If σ ∈ Tφ and φ(σ) = <a, n>, called a label node σ. If σ ∈ Tφ φ(σ)↑, we say that a node σ untagged. Partially labeled trees will be denoted by capital letters and we will write σ ∈ A is σ ∈ TA and A(α) = ⊥, when A(α)↑, but α ∈ A.
If Σ = {λx1....λxn.x | n ≥ 0, x1,..., xn, x ∈ Λ}, then a partially Σ-labeled tree is called tree Belovskogo type. The set of all such up trees denote B. a Subtree of A tree emanating from a node α is Aα = λβ.A(α * β). It is obvious that ∀A ∈ B: ∀α: Aα ∈ B.
Strategist M solvable if
∃n: ∃N1,..., Nn ∈ Λ0: M N1 ... Nn = I.
For example, the fixed point Combinator is solvable, since Y (K I) = K I (Y (K I)) = I. on the other hand, Ω is unsolvable. An arbitrary λ-expression solvable when we allow Combinator λx1....λxn.M, where {x1,..., xn} = FV(M).
λ-expression M is a head normal form if it is
M ≣ λx1....λxn.x M1 Mm, m, n ≥ 0.
Say that M is head normal form N if M = N. Main is called the head normal form of expression, which is achieved first by left reduction.
Wadsworth introduced the class of λ-expressions that do not have a head normal form, and argued in favor of the fact that the members of this class should be seen as meaningless expressions in λ-calculus. He also belongs to the following important result: λ-expression is solvable if and only if it has a head normal form. Thus, insolubility of M it follows that for any expressions N1,..., Nn expression M N1 ... Nn has no normal form.
the Tree of Bema for the term M, denoted using BT(M) is a tree Belovskogo types are defined as follows:
1) if M is unsolvable, then ∀σ: BT(Μ)(σ)↑,
2) if M is solvable and has a principal head normal form λx1....λxn.x M0 Mm — 1,
BT(M)(< >) = <λx1....λxn.x m>;
k < m ⇒ BT(M)(<k> * σ) = BT(Mk)(σ);
k ≥ m ⇒ BT(M)(<k> * σ)↑.
Consider a complete partially ordered set B = (B, ⊆) with the Scott topology. Topology of the trees on the set of Λ is the smallest topology in which continuously displays BT: Λ → B. in Other words, open subsets of Λ have the form BT-1(O), where O is open in the Scott topology on B.
Using the topology tree, one can Express the usual notions related to λ-calculus in topological terms. For example, the normal forms are isolated points, and insoluble expression — points compactification, that is, those points, the only neighborhood which is itself a topological space.
It is proved that the application and abstraction of continuous in the topology of the trees on Λ, and for an application is a nontrivial result that has interesting consequences. For example, the set Sol ⊆ Λ-solvable terms is open. Indeed, in any complete poset the set {x | x ≠ ⊥} is open on Scott. Consequently, many Sol = BT-1{A | A ≠ ⊥} is open in Λ.
Комментарии
Отправить комментарий