Extensibella Example: lambda_calculus:host

Language Specification

File: syntax.sos

[Reduce File] [Raw File] 
Module lambda_calculus:host

e ::= var(string)
    | abs(string, e)
    | app(e, e)
    | intE(int)
    | plus(e, e)

Projection e :

File: eval.sos

[Reduce File] [Raw File] 
Module lambda_calculus:host

Judgment eval : e* e

------------------------------ [E-Abs]
eval abs(X, Body) abs(X, Body)


eval E1 abs(X, Body)
eval E2 V2
subst X V2 Body B
eval B V
-------------------- [E-App]
eval app(E1, E2) V


-------------------- [E-Int]
eval intE(I) intE(I)


eval E1 intE(I1)
eval E2 intE(I2)
I1 + I2 = I
------------------------- [E-Plus]
eval plus(E1, E2) intE(I)


Extensibella_Stand_In {
  |{e}- E ~~> E_T
  eval E_T V
  --------------- [E-Q]
  eval E V
}



Judgment subst : string e e* e

------------------ [S-Var-Eq]
subst X R var(X) R


X != Y
----------------------- [S-Var-NEq]
subst X R var(Y) var(Y)


----------------------------------- [S-Abs-Eq]
subst X R abs(X, Body) abs(X, Body)


X != Y
subst X R Body B
-------------------------------- [S-Abs-NEq]
subst X R abs(Y, Body) abs(Y, B)


subst X R E1 S1
subst X R E2 S2
--------------------------------- [S-App]
subst X R app(E1, E2) app(S1, S2)


------------------------- [S-Int]
subst X R intE(I) intE(I)


subst X R E1 S1
subst X R E2 S2
----------------------------------- [S-Plus]
subst X R plus(E1, E2) plus(S1, S2)

Reasoning

[Show All Proofs] [Hide All Proofs] [Raw File]

Click on a command or tactic to see a detailed view of its use.

Module lambda_calculus:host.

Projection_Constraint proj_is : forall E E',
  |{e}- E ~~> E' -> is_e E -> is_e E'.


%Generally a good idea to include this so extensions can prove things
%based on the structure of a term
Proj_Rel is_e E.
Ext_Ind forall E, is_e E. [Show Proof]



Projection_Constraint proj_same : forall E E1 E2,
  |{e}- E ~~> E1 -> |{e}- E ~~> E2 -> E1 = E2.


Extensible_Theorem
  subst_exists : forall X R E,
    IsE : is_e E ->
    IsX : is_string X ->
    IsR : is_e R ->
    exists S, subst X R E S
  on IsE. [Show Proof]



Extensible_Theorem
  subst_is : forall X R E S,
    IsE : is_e E ->
    IsX : is_string X ->
    IsR : is_e R ->
    S : subst X R E S ->
    is_e S
  on S. [Show Proof]



Extensible_Theorem
  eval_is : forall E V,
    IsE : is_e E ->
    Ev : eval E V ->
    is_e V
  on Ev. [Show Proof]



Extensible_Theorem
  subst_unique : forall X R E SA SB,
    IsE : is_e E ->
    IsX : is_string X ->
    IsR : is_e R ->
    SA : subst X R E SA ->
    SB : subst X R E SB ->
    SA = SB
  on SA. [Show Proof]



Extensible_Theorem
  eval_unique : forall E VA VB,
    IsE : is_e E ->
    EvA : eval E VA ->
    EvB : eval E VB ->
    VA = VB
  on EvA. [Show Proof]



%anything evaluation-related must be the same across projection
Projection_Constraint proj_subst : forall X R E S E',
  Proj : |{e}- E ~~> E' ->
  IsE : is_e E ->
  IsX : is_string X ->
  IsR : is_e R ->
  S : subst X R E S ->
  exists S', subst X R E' S'.
Projection_Constraint proj_subst_same : forall X R E S E' S',
  Proj : |{e}- E ~~> E' ->
  IsE : is_e E ->
  IsX : is_string X ->
  IsR : is_e R ->
  S : subst X R E S ->
  S' : subst X R E' S' ->
  S = S'.

Projection_Constraint proj_eval : forall E E' V,
  Proj : |{e}- E ~~> E' ->
  IsE : is_e E ->
  Ev : eval E V ->
  exists V', eval E' V'.
Projection_Constraint proj_eval_same : forall E E' V V',
  Proj : |{e}- E ~~> E' ->
  IsE : is_e E ->
  Ev : eval E V ->
  Ev' : eval E' V' ->
  V = V'.


Ext_Size eval E V.
Proj_Rel eval E V.

Ext_Ind forall E V, eval E V. [Show Proof]
Back to example home