changed "the lambda-calculus" to "strong call-by-name lambda-calculus"

uds-psl · Aug 24, 2023 · 2cc7a3d · 2cc7a3d
1 parent 51c85f3
commit 2cc7a3d
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/README.md b/README.md
@@ -97,7 +97,7 @@ An equivalence proof that most of the mentioned models of computation compute th
 - Uniform boundedness of deterministic, length-preserving stack machines (`SMNdl_UB` in [`StackMachines/SMN.v`](theories/StackMachines/SMN.v))
 - Semi-unification (`SemiU` in [`SemiUnification/SemiU.v`](theories/SemiUnification/SemiU.v))
 - Halting problem for Krivine machines (`KrivineM_HALT` in [`LambdaCalculus/Krivine.v`](theories/LambdaCalculus/Krivine.v))
-- Strong normalization wrt. beta-reduction for given terms in the lambda-calculus (`SNclosed` in [`LambdaCalculus/Lambda.v`](theories/LambdaCalculus/Lambda.v))
+- Strong normalization for given terms in the strong call-by-name lambda-calculus (`SNclosed` in [`LambdaCalculus/Lambda.v`](theories/LambdaCalculus/Lambda.v))
 - System F Inhabitation (`SysF_INH` in [`SystemF/SysF.v`](theories/SystemF/SysF.v)), System F Typability (`SysF_TYP` in [`SystemF/SysF.v`](theories/SystemF/SysF.v)), System F Type Checking (`SysF_TC` in [`SystemF/SysF.v`](theories/SystemF/SysF.v))
 - Intersection Type Inhabitation (`CD_INH` in [`IntersectionTypes/CD.v`](theories/IntersectionTypes/CD.v)), Intersection Type Typability (`CD_TYP` in [`IntersectionTypes/CD.v`](theories/IntersectionTypes/CD.v)), Intersection Type Type Checking (`CD_TC` in [`IntersectionTypes/CD.v`](theories/IntersectionTypes/CD.v))
 

diff --git a/theories/L/L.v b/theories/L/L.v
@@ -1,4 +1,4 @@
-(** * Halting problem for the call-by-value lambda-calculus HaltL  *)
+(** * Halting problem for the weak call-by-value lambda-calculus HaltL  *)
 
 (* * The call-by-value lambda calculus L *)
 

diff --git a/theories/L/Reductions/HaltL_to_HaltLclosed.v b/theories/L/Reductions/HaltL_to_HaltLclosed.v
@@ -3,7 +3,7 @@ Require Import Undecidability.Synthetic.Definitions.
 From Undecidability.L Require Import L Functions.Eval Util.L_facts.
 Import L_Notations.
 
-(* Halting problem for call-by-value lambda-calculus *)
+(* Halting problem for weak call-by-value lambda-calculus *)
 Definition HaltLclosed (s : {s : term | closed s}) := exists t, eval (proj1_sig s) t.
 
 Lemma reduction : HaltL ⪯ HaltLclosed.

diff --git a/theories/LambdaCalculus/Lambda.v b/theories/LambdaCalculus/Lambda.v
@@ -49,7 +49,7 @@ Fixpoint subst (sigma: nat -> term) (s: term) : term :=
 
 Notation closed t := (forall (sigma: nat -> term), subst sigma t = t).
 
-(* beta-reduction *)
+(* beta-reduction (strong call-by-name reduction) *)
 Inductive step : term -> term -> Prop :=
   | stepSubst s t   : step (app (lam s) t) (subst (scons t (fun x => var x)) s)
   | stepAppL s s' t : step s s' -> step (app s t) (app s' t)

diff --git a/theories/LambdaCalculus/Lambda_undec.v b/theories/LambdaCalculus/Lambda_undec.v
@@ -8,7 +8,7 @@
 (*
   Undecidability Result(s):
     Weak call-by-name leftmost outermost normalization for given closed lambda-terms (wCBNclosed)
-    Strong normalization for given closed lambda-terms (SNclosed)
+    Strong normalization for given closed lambda-terms in the strong call-by-name lambda-calculus (SNclosed)
 *)
 
 From Undecidability.Synthetic Require Import Undecidability ReducibilityFacts.
@@ -32,7 +32,7 @@ Qed.
 
 Check wCBNclosed_undec.
 
-(* Undecidability of strong normalization wrt. beta-reduction for given closed lamda-terms *)
+(* Undecidability of strong normalization for given closed lamda-terms in the strong call-by-name lambda-calculus *)
 Theorem SNclosed_undec : undecidable SNclosed.
 Proof.
   apply (undecidability_from_reducibility KrivineMclosed_HALT_undec).