ABCDEFGHIJKLMNOPQRSTUVWXYZ
1
S-K Ordinal NotationVerbose SKON
2
Alphabet: {S,K,I,W,@}Alphabet: {S,K,I,W,(,)}
3
TermsTerms
4
S,K,I,W are terms
5
If x,y are terms, so is @xyIf x,y are terms, so is xy or something like that idkWell, VSKON is meant to be less formal and more for humans and so BTW I think the proper rule is (xy)
6
Denotational semanticsDenotational semantics
7
S,K,I denote the standard combinators
8
W denotes applying the first argument to the second w times
9
@ denotes function application (prefix operator)Function application is denoted like in SKIAlso parens are left-associative
10
OrdinalsOrdinals
11
An ordinal is a term which is a function applying the first to the second a timesBasically Church numerals
12
Its value is then defined to be a
13
Formal ordinalsFormal ordinals
14
Let A denote successor
15
x is the value of @@xA0, where 0 represents, well, 0x is the value of xA0
16
Beta-reductions go normally
17
@Ax=x+1Ax=x+1
18
<@xy>[n]=@<x[n]>y<xy>[n]=<x[n]>y
19
<@@Wxy>[n]=@x@x@x...y (with n @x)<Wxy>[n]=x(x(...y...)) (with n x)
20
21
I think these work
22
23
Also
24
Iota ordinal notation and verbose ION are similar
25
Replace SKI by I=S(SS(K(KK)))(KS)
26
(or @@S@@SS@K@KK@KS)
27
28
Oh, and Lambda Ordinal Notation is related (and of course Verbose LON)
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100