blob: 686f645d5d83aebcde91c32eb09aaa8b6e124652 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
{-# OPTIONS --safe #-}
module Problem11 where
data Term : Set where
Ref : Term
Sop : Term
Kop : Term
App : Term → Term → Term
variable M N P M₁ M₂ M₃ N₁ N₂ : Term
data _↦_ : Term → Term → Set where
red-S : (App (App (App Sop M) N) P) ↦ (App (App M P) (App N P))
red-K : (App (App Kop M) N) ↦ M
red-left : M₁ ↦ M₂ → App M₁ N ↦ App M₂ N
red-right : N₁ ↦ N₂ → App M N₁ ↦ App M N₂
red-trans : M ↦ N → N ↦ P → M ↦ P
open import Relation.Binary.Reasoning.Base.Partial _↦_ red-trans
ident : Term
ident = App (App Sop Kop) Kop
ident-red : App ident M ↦ M
ident-red {M} = begin
App (App (App Sop Kop) Kop) M ∼⟨ red-S ⟩
App (App Kop M) (App Kop M) ∼⟨ red-K ⟩
M ∎
const-sop : Term
const-sop = App Kop Sop
const-sop-red : App const-sop M ↦ Sop
const-sop-red = red-K
const-kop : Term
const-kop = App Kop Kop
const-kop-red : App const-kop M ↦ Kop
const-kop-red = red-K
app-app : Term → Term → Term
app-app M N = App (App Sop M) N
app-app-red : App (app-app M₁ M₂) M₃ ↦ App (App M₁ M₃) (App M₂ M₃)
app-app-red = red-S
lambda : Term → Term
lambda Ref = ident
lambda Sop = App Kop Sop
lambda Kop = App Kop Kop
lambda (App M N) = app-app (lambda M) (lambda N)
substitution : Term → Term → Term
substitution Ref N = N
substitution Sop N = Sop
substitution Kop N = Kop
substitution (App M₁ M₂) N = App (substitution M₁ N) (substitution M₂ N)
beta : ∀ M N → (App (lambda M) N) ↦ (substitution M N)
beta Ref N = ident-red
beta Sop N = const-sop-red
beta Kop N = const-kop-red
beta (App M₁ M₂) N = begin
App (app-app (lambda M₁) (lambda M₂)) N ∼⟨ app-app-red ⟩
App (App (lambda M₁) N) (App (lambda M₂) N) ∼⟨ red-left (beta M₁ N) ⟩
App (substitution M₁ N) (App (lambda M₂) N) ∼⟨ red-right (beta M₂ N) ⟩
App (substitution M₁ N) (substitution M₂ N) ∎
|
