-
Notifications
You must be signed in to change notification settings - Fork 1
/
budge-pl.btp
61 lines (48 loc) · 1.75 KB
/
budge-pl.btp
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
# Rules for creating a pair (list) and numbers (succ, pred)
rMkPair : (x y)
rTmNil : NIL
rTm0 : 0
rTmS : Sx
rTmP : Px
# Appending lists
rAppendNil : APPEND NIL y y
rAppendRec : APPEND x y z -> APPEND (a x) y (a z)
## Two-register Budge rules ##
# Initial program
rInitState : p (a b)
# Commands 1, -1, 2, -2 respectively
rNextState+1 : (S0 x) (a b) -> x (Sa b)
rNextState-1 : (P0 x) (Sa b) -> x (a b)
rNextState+2 : (SS0 x) (a b) -> x (a Sb)
rNextState-2 : (PP0 x) (a Sb) -> x (a b)
# Commands for looping on the second register
rLoop2Base : ((SS0 x) y) (a 0) -> y (a 0)
rLoop2Succ : ((SS0 x) y) (a Sb) -> APPEND x ((SS0 x) y) z -> z (a Sb)
# Proofs begin here
# Terms (numbers) we need for the proofs
t0! : rTm0
t-1! : rTmP x=t0!
t-2! : rTmP x=t-1!
t1! : rTmS x=t0!
t2! : rTmS x=t1!
t3! : rTmS x=t2!
tNil! : rTmNil
# Represent the program ((2,-2,1)), with some extra terms needed for the proofs
tEgList1! : rMkPair x=t1!;y=tNil!
tEgList2! : rMkPair x=t-2!;y=tEgList1!
tEgList3! : rMkPair x=t2!;y=tEgList2!
tEgList : rMkPair x=tEgList3!;y=tNil!
tEgList4! : rMkPair x=t-2!;y=tNil!
tEgList5! : rMkPair x=t1!;y=tEgList
tEgList6! : rMkPair x=t-2!;y=tEgList5!
tAp1! : rAppendNil y=tEgList
tAp2! : rAppendRec x=tNil!;y=tEgList;z=tEgList;a=t1! tAp1!
tAp : rAppendRec x=tEgList1!;y=tEgList;z=tEgList5!;a=t-2! tAp2!
t1Init : rInitState p=tEgList;a=t1!;b=t2!
t1Loop1 : rLoop2Succ x=tEgList2!;y=tNil!;a=t1!;b=t1!;z=tEgList6! t1Init tAp
t1DecR2 : rNextState-2 x=tEgList5!;a=t1!;b=t1! t1Loop1
t1IncR1 : rNextState+1 x=tEgList;a=t1!;b=t1! t1DecR2
t1Loop2 : rLoop2Succ x=tEgList2!;y=tNil!;a=t2!;b=t0!;z=tEgList6! t1IncR1 tAp
t1DecR2' : rNextState-2 x=tEgList5!;a=t2!;b=t0! t1Loop2
t1IncR1' : rNextState+1 x=tEgList;a=t2!;b=t0! t1DecR2'
t1 : rLoop2Base x=tEgList2!;y=tNil!;a=t3!;b=t0! t1IncR1'