Notation for modules (as in Coq modules)

Clash Royale CLAN TAG#URR8PPP

up vote
0
down vote

favorite

Wondering if there is a math notation for "modules", such as in Coq modules:

Module Type Sig.
Parameter A : Type.
Parameter le : A ⇒ A ⇒ Prop.
Infix "≤" := le : order_scope.
Open Scope order_scope.
Axiom le_refl : ∀ x, x ≤ x.
Axiom le_antisym : ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y.
Axiom le_trans : ∀ x y z, x ≤ y ⇒ y ≤ z ⇒ x ≤ z.
Axiom le_total : ∀ x y, x ≤ y + y ≤ x.
Parameter le_dec : ∀ x y, x ≤ y +¬ x ≤ y.
End Sig.

Here, you define basically a block of equations in a module. Wondering if there is any equivalent math notation for this sort of thing.

notation

share|cite|improve this question

asked Aug 3 at 13:10

Lance Pollard

1,090723

add a comment | 

up vote
0
down vote

favorite

Wondering if there is a math notation for "modules", such as in Coq modules:

Module Type Sig.
Parameter A : Type.
Parameter le : A ⇒ A ⇒ Prop.
Infix "≤" := le : order_scope.
Open Scope order_scope.
Axiom le_refl : ∀ x, x ≤ x.
Axiom le_antisym : ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y.
Axiom le_trans : ∀ x y z, x ≤ y ⇒ y ≤ z ⇒ x ≤ z.
Axiom le_total : ∀ x y, x ≤ y + y ≤ x.
Parameter le_dec : ∀ x y, x ≤ y +¬ x ≤ y.
End Sig.

Here, you define basically a block of equations in a module. Wondering if there is any equivalent math notation for this sort of thing.

notation

share|cite|improve this question

asked Aug 3 at 13:10

Lance Pollard

1,090723

add a comment | 

up vote
0
down vote

favorite

up vote
0
down vote

favorite

Wondering if there is a math notation for "modules", such as in Coq modules:

Module Type Sig.
Parameter A : Type.
Parameter le : A ⇒ A ⇒ Prop.
Infix "≤" := le : order_scope.
Open Scope order_scope.
Axiom le_refl : ∀ x, x ≤ x.
Axiom le_antisym : ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y.
Axiom le_trans : ∀ x y z, x ≤ y ⇒ y ≤ z ⇒ x ≤ z.
Axiom le_total : ∀ x y, x ≤ y + y ≤ x.
Parameter le_dec : ∀ x y, x ≤ y +¬ x ≤ y.
End Sig.

Here, you define basically a block of equations in a module. Wondering if there is any equivalent math notation for this sort of thing.

notation

share|cite|improve this question

asked Aug 3 at 13:10

Lance Pollard

1,090723

Wondering if there is a math notation for "modules", such as in Coq modules:

Module Type Sig.
Parameter A : Type.
Parameter le : A ⇒ A ⇒ Prop.
Infix "≤" := le : order_scope.
Open Scope order_scope.
Axiom le_refl : ∀ x, x ≤ x.
Axiom le_antisym : ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y.
Axiom le_trans : ∀ x y z, x ≤ y ⇒ y ≤ z ⇒ x ≤ z.
Axiom le_total : ∀ x y, x ≤ y + y ≤ x.
Parameter le_dec : ∀ x y, x ≤ y +¬ x ≤ y.
End Sig.

Here, you define basically a block of equations in a module. Wondering if there is any equivalent math notation for this sort of thing.

notation

share|cite|improve this question

asked Aug 3 at 13:10

Lance Pollard

1,090723

share|cite|improve this question

share|cite|improve this question

asked Aug 3 at 13:10

Lance Pollard

1,090723

asked Aug 3 at 13:10

Lance Pollard

1,090723

asked Aug 3 at 13:10

Lance Pollard

1,090723

1,090723

add a comment | 

add a comment | 

1 Answer
1

active

oldest

votes

up vote
1
down vote



accepted

I think you’re asking if “modules” as a way of organising classical mathematics exists, in which case the answer is not really.

Modules are a way of structuring things that is understandable to a computer. However, most of math is done in a way that is supposed to be interpreted by humans, so it is structured for humans where similar goals are achieved by:

• dividing material into book, papers, classes, and so on,


• dividing those further into parts, chapters, section, and so on,


• relying on our ability to infer things from context, so a parameter like above might be introduced by a sentence like “In this section, let $A$ denote any type and let $leq$ be a relation on $A$”, though it is not uncommon to repeat these assumptions (at least partially) for every lemma and theorem,


• “importing” other results by citing the relevant paper or book.

There is no strict notation for this; natural language is your friend.

The reason is probably that strict notation only becomes useful when you to start analysing an object. But studying these “modules” is not something a lot of mathematicians would be interested in, I suppose.

(If you are asking about modules as a subject of study in type theory or the theory of programming languages then I don’t know. Probably people just reuse the notation from the language they are studying.)

share|cite|improve this answer

answered 2 days ago

Eike Schulte

7211412

add a comment | 

Your Answer

StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "69"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
convertImagesToLinks: true,
noModals: false,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2871045%2fnotation-for-modules-as-in-coq-modules%23new-answer', 'question_page');

);

Post as a guest

Name Email

1 Answer
1

active

oldest

votes

1 Answer
1

active

oldest

votes

active

oldest

votes

active

oldest

votes

up vote
1
down vote



accepted

I think you’re asking if “modules” as a way of organising classical mathematics exists, in which case the answer is not really.

Modules are a way of structuring things that is understandable to a computer. However, most of math is done in a way that is supposed to be interpreted by humans, so it is structured for humans where similar goals are achieved by:

• dividing material into book, papers, classes, and so on,


• dividing those further into parts, chapters, section, and so on,


• relying on our ability to infer things from context, so a parameter like above might be introduced by a sentence like “In this section, let $A$ denote any type and let $leq$ be a relation on $A$”, though it is not uncommon to repeat these assumptions (at least partially) for every lemma and theorem,


• “importing” other results by citing the relevant paper or book.

There is no strict notation for this; natural language is your friend.

The reason is probably that strict notation only becomes useful when you to start analysing an object. But studying these “modules” is not something a lot of mathematicians would be interested in, I suppose.

(If you are asking about modules as a subject of study in type theory or the theory of programming languages then I don’t know. Probably people just reuse the notation from the language they are studying.)

share|cite|improve this answer

answered 2 days ago

Eike Schulte

7211412

add a comment | 

up vote
1
down vote



accepted

I think you’re asking if “modules” as a way of organising classical mathematics exists, in which case the answer is not really.

Modules are a way of structuring things that is understandable to a computer. However, most of math is done in a way that is supposed to be interpreted by humans, so it is structured for humans where similar goals are achieved by:

• dividing material into book, papers, classes, and so on,


• dividing those further into parts, chapters, section, and so on,


• relying on our ability to infer things from context, so a parameter like above might be introduced by a sentence like “In this section, let $A$ denote any type and let $leq$ be a relation on $A$”, though it is not uncommon to repeat these assumptions (at least partially) for every lemma and theorem,


• “importing” other results by citing the relevant paper or book.

There is no strict notation for this; natural language is your friend.

The reason is probably that strict notation only becomes useful when you to start analysing an object. But studying these “modules” is not something a lot of mathematicians would be interested in, I suppose.

(If you are asking about modules as a subject of study in type theory or the theory of programming languages then I don’t know. Probably people just reuse the notation from the language they are studying.)

share|cite|improve this answer

answered 2 days ago

Eike Schulte

7211412

add a comment | 

up vote
1
down vote



accepted

up vote
1
down vote



accepted

I think you’re asking if “modules” as a way of organising classical mathematics exists, in which case the answer is not really.

Modules are a way of structuring things that is understandable to a computer. However, most of math is done in a way that is supposed to be interpreted by humans, so it is structured for humans where similar goals are achieved by:

• dividing material into book, papers, classes, and so on,


• dividing those further into parts, chapters, section, and so on,


• relying on our ability to infer things from context, so a parameter like above might be introduced by a sentence like “In this section, let $A$ denote any type and let $leq$ be a relation on $A$”, though it is not uncommon to repeat these assumptions (at least partially) for every lemma and theorem,


• “importing” other results by citing the relevant paper or book.

There is no strict notation for this; natural language is your friend.

The reason is probably that strict notation only becomes useful when you to start analysing an object. But studying these “modules” is not something a lot of mathematicians would be interested in, I suppose.

(If you are asking about modules as a subject of study in type theory or the theory of programming languages then I don’t know. Probably people just reuse the notation from the language they are studying.)

share|cite|improve this answer

answered 2 days ago

Eike Schulte

7211412

I think you’re asking if “modules” as a way of organising classical mathematics exists, in which case the answer is not really.

Modules are a way of structuring things that is understandable to a computer. However, most of math is done in a way that is supposed to be interpreted by humans, so it is structured for humans where similar goals are achieved by:

• dividing material into book, papers, classes, and so on,


• dividing those further into parts, chapters, section, and so on,


• relying on our ability to infer things from context, so a parameter like above might be introduced by a sentence like “In this section, let $A$ denote any type and let $leq$ be a relation on $A$”, though it is not uncommon to repeat these assumptions (at least partially) for every lemma and theorem,


• “importing” other results by citing the relevant paper or book.

There is no strict notation for this; natural language is your friend.

The reason is probably that strict notation only becomes useful when you to start analysing an object. But studying these “modules” is not something a lot of mathematicians would be interested in, I suppose.

(If you are asking about modules as a subject of study in type theory or the theory of programming languages then I don’t know. Probably people just reuse the notation from the language they are studying.)

share|cite|improve this answer

answered 2 days ago

Eike Schulte

7211412

share|cite|improve this answer

share|cite|improve this answer

answered 2 days ago

Eike Schulte

7211412

answered 2 days ago

Eike Schulte

7211412

answered 2 days ago

Eike Schulte

7211412

7211412

add a comment | 

add a comment | 

 

draft saved

draft discarded

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2871045%2fnotation-for-modules-as-in-coq-modules%23new-answer', 'question_page');

);

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Name Email

Name

Email

Name Email

Name

Email