From ef4b2f27f2bca3ab194bbe37412e5fdf67720f30 Mon Sep 17 00:00:00 2001 From: Walter Schulze Date: Wed, 28 Aug 2024 09:29:43 +0100 Subject: [PATCH 1/4] table of renamings --- Katydid/Conal/Readme.md | 42 +++++++++++++++++++++++++++++++++++++---- 1 file changed, 38 insertions(+), 4 deletions(-) diff --git a/Katydid/Conal/Readme.md b/Katydid/Conal/Readme.md index 167df96..30cc602 100644 --- a/Katydid/Conal/Readme.md +++ b/Katydid/Conal/Readme.md @@ -17,10 +17,44 @@ The goals of this project are to: Simply renamings: - - `Set` in Agda is `Type` in Lean. - - universe levels is `ℓ` in Agda and `u` in Lean. - - parametric types in Agda is `A` and `\alpha` in Lean. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
DescriptionOriginal AgdaTranslated Lean
`Set``Type`
universe levels`ℓ`, 'b'`u`, 'v'
parametric types`A`, `B``α`, `β`
Isomorphism`↔``<=>`
Exetensional Isomorphism`⟷``∀ {w: List α}, (a w) <=> (b w)`
+ +Syntax: + + - We dropped most of the syntax, in favour of `([a-z]|[A-Z]|')` names. + - We use namespaces as much as possible to make dependencies clear to the reader without requiring "Go to Definition" and Lean to be installed. Not just a renaming, but still a difference with little consequence: - - `Lang` in Agda is defined as `Lang \alpha` in Lean. The `A` parameter for `Lang` is lifted to the module level in Agda, but there doesn't seem to be a way to hide this in Lean. + - `Lang` in Agda is defined as `Lang α` in Lean. The `A` parameter for `Lang` is lifted to the module level in Agda, but there doesn't seem to be a way to hide this in Lean. From b200df3557925bcf29cadb887f6656972cf17871 Mon Sep 17 00:00:00 2001 From: Walter Schulze Date: Wed, 28 Aug 2024 09:35:44 +0100 Subject: [PATCH 2/4] update table --- Katydid/Conal/Readme.md | 40 ++++++++-------------------------------- 1 file changed, 8 insertions(+), 32 deletions(-) diff --git a/Katydid/Conal/Readme.md b/Katydid/Conal/Readme.md index 30cc602..4c07732 100644 --- a/Katydid/Conal/Readme.md +++ b/Katydid/Conal/Readme.md @@ -17,38 +17,14 @@ The goals of this project are to: Simply renamings: - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
DescriptionOriginal AgdaTranslated Lean
`Set``Type`
universe levels`ℓ`, 'b'`u`, 'v'
parametric types`A`, `B``α`, `β`
Isomorphism`↔``<=>`
Exetensional Isomorphism`⟷``∀ {w: List α}, (a w) <=> (b w)`
+| Description | Original Agda | Translated Lean | +| :--- | :---: | :---: | +| Content | Content | Content | +| | `Set` | `Type` | +| universe levels | `ℓ`, `b` | `u`, `v` | +| parametric types | `A`, `B` | `α`, `β` | +| isomorphism | `↔` | `<=>` | +| extensional isomorphism | `⟷` | `∀ {w: List α}, (P w) <=> (Q w)` | Syntax: From c8190f5a265f89ebbda7b53aa42731d4edda2d4f Mon Sep 17 00:00:00 2001 From: Walter Schulze Date: Wed, 28 Aug 2024 10:09:50 +0100 Subject: [PATCH 3/4] more notation tables --- Katydid/Conal/Decidability.lean | 4 +-- Katydid/Conal/Readme.md | 49 ++++++++++++++++++++++++++++----- 2 files changed, 44 insertions(+), 9 deletions(-) diff --git a/Katydid/Conal/Decidability.lean b/Katydid/Conal/Decidability.lean index ea4e1ab..212874e 100644 --- a/Katydid/Conal/Decidability.lean +++ b/Katydid/Conal/Decidability.lean @@ -64,7 +64,7 @@ def list? {α: Type u}: Dec α -> Dec (List α) := -- map′ : (A → B) → (B → A) → Dec A → Dec B -- map′ A→B B→A (yes a) = yes (A→B a) -- map′ A→B B→A (no ¬a) = no (¬a ∘ B→A) -def map' {α β: Type u} (ab: α -> β) (ba: β -> α) (deca: Dec α): Dec β := +private def map' {α β: Type u} (ab: α -> β) (ba: β -> α) (deca: Dec α): Dec β := match deca with | Dec.yes a => Dec.yes (ab a) @@ -73,7 +73,7 @@ def map' {α β: Type u} (ab: α -> β) (ba: β -> α) (deca: Dec α): Dec β := -- map‽⇔ : A ⇔ B → Dec A → Dec B -- map‽⇔ A⇔B = map′ (to ⟨$⟩_) (from ⟨$⟩_) where open Equivalence A⇔B -def map? {α β: Type u} (ab: α <=> β) (deca: Dec α): Dec β := +private def map? {α β: Type u} (ab: α <=> β) (deca: Dec α): Dec β := map' ab.toFun ab.invFun deca -- _▹_ : A ↔ B → Dec A → Dec B diff --git a/Katydid/Conal/Readme.md b/Katydid/Conal/Readme.md index 4c07732..47c44d7 100644 --- a/Katydid/Conal/Readme.md +++ b/Katydid/Conal/Readme.md @@ -15,22 +15,57 @@ The goals of this project are to: ## Differences with Agda implementation -Simply renamings: +### Simply renamings + +Some things we renamed since they are simply called different things in Agda and Lean, while others were renamed to be closer to the Lean convention. | Description | Original Agda | Translated Lean | | :--- | :---: | :---: | -| Content | Content | Content | | | `Set` | `Type` | | universe levels | `ℓ`, `b` | `u`, `v` | | parametric types | `A`, `B` | `α`, `β` | | isomorphism | `↔` | `<=>` | | extensional isomorphism | `⟷` | `∀ {w: List α}, (P w) <=> (Q w)` | -Syntax: +### Namespaces / Qualified Imports + +We use namespaces as much as possible to make dependencies clear to the reader without requiring "Go to Definition" and Lean to be installed. + +| Description | Original Agda | Translated Lean | +| :--- | :---: | :---: | +| `List α -> Type u` | `◇.Lang` | `Language.Lang` | +| `List α -> β` | `◇.ν` | `Calculus.null` | +| `(List α -> β) -> (a: α) -> (List α -> β)` | `◇.δ` | `Calculus.derive` | +| | `Dec` | `Decidability.Dec` | + +### Syntax + +We dropped most of the syntax, in favour of `([a-z]|[A-Z]|')` names. + +| Description | Original Agda | Translated Lean | +| :--- | :---: | :---: | +| Content | Content | Content | +| nullable | `ν` | `null` | +| derivative of a string | `𝒟` | `derives` | +| derivative of a character | `δ` | `derive` | +| | `∅` | `emptyset` | +| | `𝒰` | `universal` | +| empty string | `𝟏` | `emptystr` | +| character | ` c | `char c` | +| | `∪` | `or` | +| | `∩` | `and` | +| scalar | `s · P` | `scalar s P` | +| | `P ⋆ Q` | `concat P Q` | +| zero or more | `P ☆` | `star P` | +| decidable bottom | `⊥?` | `Decidability.empty?` | +| decidable top | `⊤‽` | `Decidability.unit?` | +| decidable sum | `_⊎‽_` | `Decidability.sum?` | +| decidable prod | `_×‽_` | `Decidability.prod?` | +| `Dec α -> Dec (List α)` | `_✶‽` | `Decidability.list?` | +| `(β <=> α) -> Dec α -> Dec β` | `◃` | `Decidability.apply'` | - - We dropped most of the syntax, in favour of `([a-z]|[A-Z]|')` names. - - We use namespaces as much as possible to make dependencies clear to the reader without requiring "Go to Definition" and Lean to be installed. +All language operators defined in `Language.lagda` are referenced in other modules as `◇.∅`, while in Lean they are references as qualified and non notational names `Language.emptyset`. The exception is `Calculus.lean`, where `Language.lean` is opened, so they are not qualified. -Not just a renaming, but still a difference with little consequence: +### Explicit parameters. - - `Lang` in Agda is defined as `Lang α` in Lean. The `A` parameter for `Lang` is lifted to the module level in Agda, but there doesn't seem to be a way to hide this in Lean. +We use explicit parameters and almost no module level parameters, for example `Lang` in Agda is defined as `Lang α` in Lean. In Agda the `A` parameter for `Lang` is lifted to the module level, but in this translation we make it explicit. From faf837046ca0d1945554141e430e2bba7a01d231 Mon Sep 17 00:00:00 2001 From: Walter Schulze Date: Wed, 28 Aug 2024 10:10:26 +0100 Subject: [PATCH 4/4] fix table --- Katydid/Conal/Readme.md | 1 - 1 file changed, 1 deletion(-) diff --git a/Katydid/Conal/Readme.md b/Katydid/Conal/Readme.md index 47c44d7..88fa31b 100644 --- a/Katydid/Conal/Readme.md +++ b/Katydid/Conal/Readme.md @@ -44,7 +44,6 @@ We dropped most of the syntax, in favour of `([a-z]|[A-Z]|')` names. | Description | Original Agda | Translated Lean | | :--- | :---: | :---: | -| Content | Content | Content | | nullable | `ν` | `null` | | derivative of a string | `𝒟` | `derives` | | derivative of a character | `δ` | `derive` |