From 2122ea1010236126ac288cd9ead56d7bb92c9df2 Mon Sep 17 00:00:00 2001 From: Marc-Antoine Ouimet Date: Mon, 29 Jan 2024 22:16:22 -0500 Subject: [PATCH] Remove usages of MathJax in examples The MathJax CDN on `http://cdn.mathjax.org` was retired in 2017. --- .../literate_beluga/0Beginner/Close_Terms.bel | 2 +- examples/literate_beluga/0Beginner/Norm.bel | 6 +++--- ...lgorithmic_Equality_-_Context_Relation.bel | 3 ++- ...rithmic_Equality_-_Context_Subsumption.bel | 1 + .../1Intermediate/Poplmark.bel | 19 ++++++------------- .../2Advanced/Normalization_by_Evaluation.bel | 11 ++--------- .../2Advanced/Weak_Normalization.bel | 2 +- 7 files changed, 16 insertions(+), 28 deletions(-) diff --git a/examples/literate_beluga/0Beginner/Close_Terms.bel b/examples/literate_beluga/0Beginner/Close_Terms.bel index c5a9e03eb..cccd3e362 100644 --- a/examples/literate_beluga/0Beginner/Close_Terms.bel +++ b/examples/literate_beluga/0Beginner/Close_Terms.bel @@ -7,7 +7,7 @@ %{{ # Closing terms with free variables -We'll first defining what terms are in the untyped lambda calculus. +We'll first be defining what terms are in the untyped lambda calculus. }}% LF tm : type = diff --git a/examples/literate_beluga/0Beginner/Norm.bel b/examples/literate_beluga/0Beginner/Norm.bel index 642bed3d0..172f6868f 100644 --- a/examples/literate_beluga/0Beginner/Norm.bel +++ b/examples/literate_beluga/0Beginner/Norm.bel @@ -1,8 +1,8 @@ % Author: Brigitte Pientka + %{{ -# Normalizing lambda-terms -}}% -%{{ +# Normalizing lambda-Terms + ## Syntax We define first intrinsically well-typed lambda-terms using the base type `nat` and function type. }}% diff --git a/examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Relation.bel b/examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Relation.bel index 39de6b68b..f199921ba 100755 --- a/examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Relation.bel +++ b/examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Relation.bel @@ -1,5 +1,6 @@ %{{ -$Algorithmic Equality for the Untyped Lambda-calculus (R-version) +# Algorithmic Equality for the Untyped Lambda-calculus (R-version) + We discuss completeness of algorithmic equality for untyped lambda-terms with respect to declarative equality of lambda-terms. This case-study is part of [ORBI](https://github.com/pientka/ORBI), Open challenge problem Repository for systems reasoning with Binders. For a detailed description of the proof and a discussion regarding other systems see (Felty et al, 2014). diff --git a/examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Subsumption.bel b/examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Subsumption.bel index 45ec585a7..6c2313afc 100755 --- a/examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Subsumption.bel +++ b/examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Subsumption.bel @@ -3,6 +3,7 @@ % %{{ # Algorithmic Equality for the Untyped Lambda-calculus (Generalized context version) + We discuss completeness of algorithmic equality for untyped lambda-terms with respect to declarative equality of lambda-terms. This case-study is part of ORBI, Open challenge problem Repository for systems reasoning with Binders. For a detailed description of the proof and a discussion regarding other systems see (Felty et al, 2014). diff --git a/examples/literate_beluga/1Intermediate/Poplmark.bel b/examples/literate_beluga/1Intermediate/Poplmark.bel index cfb9e9055..a765346bc 100644 --- a/examples/literate_beluga/1Intermediate/Poplmark.bel +++ b/examples/literate_beluga/1Intermediate/Poplmark.bel @@ -1,11 +1,4 @@ %{{ - - - # Transitivity of Algorithmic Subtyping This example follows the proof in the proof pearl description which appeared at TPHOLs2007 @@ -33,7 +26,7 @@ for type variables, but instead we provide for each type variable its own reflexivity and transitivity version. In other words, our rule for polymorphic types implements the following: $$\frac{\Gamma \vdash T_1 <: S_1 \qquad \Gamma, tr:a <: U \rightarrow U <: T \rightarrow a <: T, w:a <: T, ref : a <: a \vdash S_2 <: T_2 }{\Gamma \vdash \forall a:S_1.S_2(a) <: \forall a:T_1.T_2(a)}$$ -We use ($<:$) or `sub` to denote algorithmic subtyping. +We use (\\(<:\\)) or `sub` to denote algorithmic subtyping. }}% LF sub : tp -> tp -> type = @@ -59,7 +52,7 @@ schema s_ctx = some [u:tp] block a:tp, tr:{U:tp}{T:tp} sub a U -> sub U T -> su %{{ ### Reflexivity -**Theorem** : For every $\Gamma$ and $T$, $\Gamma\vdash T <: T$. +**Theorem** : For every \\(\Gamma\\) and \\(T\\), \\(\Gamma\vdash T <: T\\). The reflexivity Theorem is simply described as `{g:s_ctx} {T: [g |- tp]} [g |- sub T T]` in computational-level in Beluga. Context variable `g` and term `T` are written explicitly using curly brackets `{g:s_ctx}` and `{T: [g |- tp]}`. @@ -85,7 +78,7 @@ rec refl : {g:s_ctx} {T: [g |- tp]} [g |- sub T T] = %{{ ### Transitivity -**Theorem** : For every $\Gamma$, $S$, $Q$ and $T$, if $\Gamma\vdash S <: Q$ and $\Gamma\vdash Q <: T$, then $\Gamma\vdash S <: T$. +**Theorem** : For every \\(\Gamma\\), \\(S\\), \\(Q\\) and \\(T\\), if \\(\Gamma\vdash S <: Q\\) and \\(\Gamma\vdash Q <: T\\), then \\(\Gamma\vdash S <: T\\). The transitivity Theorem is described as `(g:s_ctx){Q:[g |- tp]}[g |- sub S Q] -> [g |- sub Q T] -> [g |- sub S T]`. The context variable is written implicitly in round bracket as `(g:s_ctx)`. @@ -168,7 +161,7 @@ Recall `D2` is a parametric and hypothetical derivation which can be viewed as a ## Declarative subtyping We can also define declarative subtyping in Beluga and prove the equivalence between algoritmic and declarative subtyping through soundness and completeness proofs. -We use ($<$) or `subtype` to denote declarative subtyping. +We use (\\(<\\)) or `subtype` to denote declarative subtyping. }}% @@ -195,7 +188,7 @@ schema ss_ctx = some [u:tp] block a:tp, tr:{U:tp}{T:tp} sub a U -> sub U T -> su %{{ ### Soundness -**Theorem** : For every $\Gamma$, $T$ and $S$, if $\Gamma\vdash T<:S$, then $\Gamma\vdash T < S$ . +**Theorem** : For every \\(\Gamma\\), \\(T\\) and \\(S\\), if \\(\Gamma\vdash T<:S\\), then \\(\Gamma\vdash T < S\\) . }}% rec sound : (g:ss_ctx) [g |- sub T S] -> [g |- subtype T S] = @@ -230,7 +223,7 @@ rec sound : (g:ss_ctx) [g |- sub T S] -> [g |- subtype T S] = %{{ ### Completeness -**Theorem**: For every $\Gamma$, $T$ and $S$, if $\Gamma\vdash T < S$, then $\Gamma\vdash T <: S$. +**Theorem**: For every \\(\Gamma\\), \\(T\\) and \\(S\\), if \\(\Gamma\vdash T < S\\), then \\(\Gamma\vdash T <: S\\). }}% rec complete : (g:ss_ctx) [g |- subtype T S] -> [g |- sub T S] = diff --git a/examples/literate_beluga/2Advanced/Normalization_by_Evaluation.bel b/examples/literate_beluga/2Advanced/Normalization_by_Evaluation.bel index 019812844..ad11ad509 100644 --- a/examples/literate_beluga/2Advanced/Normalization_by_Evaluation.bel +++ b/examples/literate_beluga/2Advanced/Normalization_by_Evaluation.bel @@ -1,15 +1,8 @@ %{{ - - - # Normalization by Evaluation This case study shows how to implement a type-preserving normalizer using normalization by evaluation [Berger and Schwichtenberg 1991]. -Here we compute $\eta$-long normal forms for the simply-typed lambda calculus. +Here we compute \\(\eta\\)-long normal forms for the simply-typed lambda calculus. See also [Cave and Pientka 2012] for more information on this example. The setup is a standard intrinsically-typed lambda calculus: @@ -26,7 +19,7 @@ lam : (tm T -> tm S) -> tm (arr T S). schema tctx = tm T; %{{ -Below, we describe $\eta$-long normal forms. Notice that we allow embedding of neutral terms into normal terms only at base type `b`: this enforces $\eta$-longness. +Below, we describe \\(\eta\\)-long normal forms. Notice that we allow embedding of neutral terms into normal terms only at base type `b`: this enforces \\(\eta\\)-longness. }}% neut : tp -> type. --name neut R. diff --git a/examples/literate_beluga/2Advanced/Weak_Normalization.bel b/examples/literate_beluga/2Advanced/Weak_Normalization.bel index e1fb25ade..6d6695692 100644 --- a/examples/literate_beluga/2Advanced/Weak_Normalization.bel +++ b/examples/literate_beluga/2Advanced/Weak_Normalization.bel @@ -125,7 +125,7 @@ mlam MS => fn r => case r of %{{ The trivial fact that reducible terms halt has a corresponding trivial proof, analyzing the construction of the the proof of -'Reduce[|- T] [|- M]' +`Reduce [|- T] [|- M]` }}% rec reduce_halts : Reduce [|- T] [ |- M] -> [ |- halts M] =