Skip to content
May 20, 2017 / porton

The math book rewritten with implicit arguments

I have rewritten my math book (volume 1) with implicit arguments (that is I sometimes write \bot instead of \bot^{\mathfrak{A}} to denote the least element of the lattice \mathfrak{A}).

It considerably simplifies the formulas.

If you want to be on this topic, learn what is called “dependent lambda calculus”. (Sadly, I do not use it in my book explicitly, in order to make my book easier to understand. But I weight the possibility to rewrite my book in a dependent lambda calculus proof-assistant language, that is in the language of an automatic proof verification software, to make it even greater.)

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: