Skip to content

Commit

Permalink
Draft different options for reduction rules
Browse files Browse the repository at this point in the history
  • Loading branch information
@Anatolay
Anatolay committed Feb 9, 2024
1 parent 99272db commit 894b4da
Showing 1 changed file with 306 additions and 0 deletions.
306 changes: 306 additions & 0 deletions Extended/Calculus.lean
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,306 @@
set_option autoImplicit false

@[reducible]
def Attr := String
@[reducible]
def Function := String
@[reducible]
def Bytes := String

-- inductive Attr where
-- | Ο† : Attr
-- | ρ : Attr
-- | Οƒ : Attr
-- | Ξ½ : Attr
-- | Ξ± : String β†’ Attr

mutual
inductive Binder : Attr β†’ Type where
| alpha : (a : Attr) β†’ Term β†’ Binder a
| empty : (a : Attr) β†’ Binder a
| delta : Bytes β†’ Binder "Ξ”"
| lambda : Function β†’ Binder "Ξ»"

inductive Bindings : List Attr β†’ Type where
| nil : Bindings []
| cons
: { lst : List Attr }
β†’ { a : Attr }
β†’ a βˆ‰ lst
β†’ Binder a
β†’ Bindings lst
β†’ Bindings (a :: lst)

inductive Term : Type where
| obj : { attrs : List Attr } β†’ Bindings attrs β†’ Term -- ⟦ α₁ ↦ u₁, ... Ξ±β‚– ↦ uβ‚– ⟧
| app : { attrs : List Attr } β†’ Term β†’ Bindings attrs β†’ Term -- t(α₁ ↦ u₁, ... Ξ±β‚– ↦ uβ‚–)
-- | obj : Bindings _ β†’ Term
-- | app : Term β†’ Bindings _ β†’ Term
| dot : Term β†’ Attr β†’ Term -- t.a
| glob : Term -- Ξ¦
| this : Term -- ΞΎ
| termination : Term -- βŠ₯
end
open Term

namespace Bindings

def singleton (a : Attr) (t : Term) : Bindings [a]
:= cons (Ξ» isin => by contradiction) (Binder.alpha a t) nil

end Bindings

inductive IsAttached : { attrs : List Attr } β†’ Attr β†’ Term β†’ Bindings attrs β†’ Type where
-- | zeroth_attached
-- : { lst : List Attr }
-- β†’ (a : Attr)
-- β†’ (not_in : a βˆ‰ lst)
-- β†’ (t : Term)
-- β†’ (l : Bindings lst)
-- β†’ IsAttached a t (Bindings.cons a not_in (attached t) l)
-- | next_attached
-- : { lst : List Attr }
-- β†’ (a : Attr)
-- β†’ (t : Term)
-- β†’ (l : Bindings lst)
-- β†’ (b : Attr)
-- β†’ (a β‰  b)
-- β†’ (not_in : b βˆ‰ lst)
-- β†’ (u : OptionalAttr)
-- β†’ IsAttached a t l
-- β†’ IsAttached a t (Bindings.cons b not_in u l)

inductive IsVoid : { attrs : List Attr } β†’ Attr β†’ Bindings attrs β†’ Type

universe u v
inductive ForAll : { Ξ± : Type u } β†’ (f : Ξ± β†’ Type v) β†’ (List Ξ±) β†’ Prop where
| nil : { Ξ± : Type u } β†’ { f : Ξ± β†’ Type v } β†’ ForAll f []
| cons : { Ξ± : Type u } β†’ { f : Ξ± β†’ Type v } β†’ (l : List Ξ±) β†’ (a : Ξ±) β†’ (fa : f a) β†’ ForAll f l β†’ ForAll f (a :: l)

def insert
{ attrs : List Attr }
(bnds : Bindings attrs)
(a : Attr)
(u : Term)
: (Bindings attrs)
:= sorry

def remove
{ attrs : List Attr }
(bnds : Bindings attrs)
(a : Attr)
: Bindings (List.removeAll attrs [a])
:= sorry

def insertAll
{ attrs_from : List Attr }
{ attrs_to : List Attr }
(bnds_from : Bindings attrs_from)
(bnds_to : Bindings attrs_to)
: (Bindings attrs_to)
:= sorry

def subst_this_head
(t : Term)
(u : Term)
: Term
:= match t with
| obj bnds => obj bnds
| app t' bnds => app t' bnds
| dot t' a => dot (subst_this_head t' u) a
| glob => glob
| this => u
| termination => termination

inductive NormalForm : Term β†’ Type where
| nf : (t : Term) β†’ NormalForm t

inductive Prog : Type where
| prog : { attrs : List Attr } β†’ Bindings attrs β†’ Prog
def get_bindings (prog : Prog) : Ξ£ attrs : List Attr, Bindings attrs
:= match prog with
| @Prog.prog attrs bnds => ⟨attrs, bnds⟩

inductive Reduce : Prog β†’ Term β†’ Term β†’ Type where
| congDot
: { a : Attr }
β†’ { t t' : Term }
β†’ { prog : Prog }
β†’ Reduce prog t t'
β†’ Reduce prog (dot t a) (dot t' a)
| congObj
: { a : Attr }
β†’ { t t' : Term }
β†’ { prog : Prog }
β†’ { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ IsAttached a t bnds
β†’ Reduce prog t t' -- Ξ¦ ↦ ⟦B⟧ ⊒ t ⇝ t'
β†’ Reduce
prog
(obj bnds) -- ⟦ a ↦ t, B ⟧
(obj (insert bnds a t')) -- ⟦ a ↦ t', B ⟧
| r4
: { prog : Prog }
β†’ Reduce
prog -- Ξ¦ ↦ ⟦B⟧
glob -- Ξ¦
(obj (insert (get_bindings prog).snd "Οƒ" glob)) -- ⟦ B, Οƒ ↦ Ξ¦ ⟧
| r5
: { prog : Prog }
β†’ { a : Attr }
β†’ { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ (t : Term)
β†’ IsAttached a t bnds
β†’ Reduce
prog
(obj bnds) -- ⟦ a ↦ ΞΎ β€’ t', B ⟧
(obj (insert bnds a (subst_this_head t (obj bnds)))) -- ⟦ a ↦ ⟦B⟧ β€’ t', B ⟧ ?add recursion?
| r6
: { a : Attr }
β†’ { attrs : List Attr }
β†’ { bnds : Bindings attrs } -- B
β†’ (n : Term)
β†’ IsAttached a n bnds
β†’ (prog : Prog)
β†’ NormalForm n
β†’ Reduce
prog
(dot (obj bnds) a) -- ⟦ a ↦ n, B ⟧.a
(app n (Bindings.singleton "ρ" (obj (remove bnds a)))) -- n(ρ ↦ ⟦B⟧), ?should keep a ↦ n?
| r7
: { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ { void_attrs : List Attr }
β†’ ForAll (Ξ» a => IsVoid a bnds) void_attrs
β†’ (prog : Prog)
β†’ (void_bnds : Bindings void_attrs)
β†’ Reduce
prog
(app (obj bnds) void_bnds) -- ⟦ τ₁ ↦ βˆ…, Ο„β‚‚ ↦ βˆ…, ... B⟧(τ₁ ↦ n₁, Ο„β‚‚ ↦ nβ‚‚, ...)
(obj (insertAll void_bnds (remove bnds "Ξ½"))) -- ⟦ τ₁ ↦ n₁, Ο„β‚‚ ↦ nβ‚‚, ... B ─ Ξ½ ⟧
| r8
: { a : Attr }
β†’ { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ (prog : Prog)
β†’ a βˆ‰ attrs
β†’ (n : Term)
β†’ NormalForm n
β†’ IsAttached "Ο†" n bnds
β†’ Reduce
prog
(dot (obj bnds) a) -- ⟦ Ο† ↦ n, B ⟧.a
(dot n a) -- n.a
| r9
: { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ { n : Term }
β†’ (prog : Prog)
β†’ NormalForm n
β†’ Reduce
prog
(app (obj bnds) (Bindings.singleton "ρ" n)) -- ⟦ B ⟧(ρ ↦ n)
(obj (insert bnds "ρ" n)) -- ⟦ ρ ↦ n, B ─ ρ ⟧

inductive Context where
| prog : { attrs : List Attr } β†’ Bindings attrs β†’ Context
| cons : { attrs : List Attr } β†’ Bindings attrs β†’ Context β†’ Context

def top (ctx : Context) : Ξ£ attrs : List Attr, Bindings attrs
:= match ctx with
| @Context.prog a b => ⟨a, b⟩
| @Context.cons a b _ => ⟨a, b⟩

def getProg (ctx : Context) : Ξ£ attrs : List Attr, Bindings attrs
:= match ctx with
| @Context.prog a b => ⟨a, b⟩
| Context.cons _ c => getProg c

mutual
inductive Entails : Context β†’ Term β†’ Type where
-- | ???

-- infix:20 " ⊒ " => WithContext.entails
inductive ReduceCtx : Context β†’ Term β†’ Term β†’ Type where
| congDot
: { a : Attr }
β†’ { t t' : Term }
β†’ { ctx : Context }
β†’ ReduceCtx ctx t t'
β†’ ReduceCtx ctx (dot t a) (dot t' a)
| congObj
: { a : Attr }
β†’ { t t' : Term }
β†’ { ctx : Context }
β†’ { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ IsAttached a t bnds
β†’ ReduceCtx (Context.cons (remove bnds a) ctx) t t' -- ⟦B⟧ ⊒ t ⇝ t'
β†’ ReduceCtx
ctx
(obj bnds) -- ⟦ a ↦ t, B ⟧
(obj (insert bnds a t')) -- ⟦ a ↦ t', B ⟧
| r4
: { ctx : Context }
β†’ ReduceCtx
ctx -- ⟦B⟧, Ξ“
glob -- Ξ¦
(obj (insert (getProg ctx).snd "Οƒ" glob)) -- ⟦ B, Οƒ ↦ Ξ¦ ⟧
| r5
: { ctx : Context }
β†’ { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ ReduceCtx
(Context.cons bnds ctx) -- Ξ“ , ⟦ B ⟧ ?ᡃ?
this -- ΞΎ
(obj bnds) -- ⟦ B ⟧
| r6
: { a : Attr }
β†’ { attrs : List Attr }
β†’ { bnds : Bindings attrs } -- B
β†’ a βˆ‰ attrs
β†’ (n : Term)
β†’ (ctx : Context) -- Ξ“
β†’ Entails (Context.cons bnds ctx) n -- Ξ“, ⟦B⟧ ⊒ n
β†’ NormalForm n
β†’ ReduceCtx
ctx
(dot (obj (insert bnds a n)) a) -- ⟦ a ↦ n, B ⟧.a
(app n (Bindings.singleton "ρ" (obj bnds))) -- n(ρ ↦ ⟦ B ⟧), ?should add a ↦ n?
| r7
: { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ { void_attrs : List Attr }
β†’ ForAll (Ξ» a => IsVoid a bnds) void_attrs
β†’ (ctx : Context)
β†’ (void_bnds : Bindings void_attrs)
β†’ ReduceCtx
ctx
(app (obj bnds) void_bnds) -- ⟦ τ₁ ↦ βˆ…, Ο„β‚‚ ↦ βˆ…, ... B⟧(τ₁ ↦ n₁, Ο„β‚‚ ↦ nβ‚‚, ...)
(obj (insertAll void_bnds bnds)) -- ⟦ τ₁ ↦ n₁, Ο„β‚‚ ↦ nβ‚‚, ... B ⟧ todo: B ─ Ξ½
| r8
: { a : Attr }
β†’ { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ (ctx : Context)
β†’ a βˆ‰ attrs
β†’ (n : Term)
β†’ NormalForm n
β†’ IsAttached "Ο†" n bnds
β†’ ReduceCtx
ctx
(dot (obj bnds) a)
(dot n a)
| r9
: { attrs : List Attr }
β†’ { bnds : Bindings attrs }
β†’ { n : Term }
β†’ (ctx : Context)
β†’ NormalForm n
β†’ ReduceCtx
ctx
(app (obj bnds) (Bindings.singleton "ρ" n)) -- ⟦ B ⟧(ρ ↦ n)
(obj (insert bnds "ρ" n)) -- ⟦ ρ ↦ n, B ─ ρ ⟧
end

0 comments on commit 894b4da

Please sign in to comment.