Zulip Chat Archive

Stream: new members

Topic: constants and variables


view this post on Zulip Patrick Thomas (Mar 25 2019 at 02:55):

Is scoping the only difference between constants and variables in Lean?

view this post on Zulip Kenny Lau (Mar 25 2019 at 02:57):

constants are axioms while variables is just a shorthand to insert "forall" in the following theorems

view this post on Zulip Kenny Lau (Mar 25 2019 at 02:57):

so for example classical.choice is a constant

view this post on Zulip Patrick Thomas (Mar 25 2019 at 03:00):

"forall" as an assumed hypothesis in all the following theorems?

view this post on Zulip Patrick Thomas (Mar 25 2019 at 03:02):

I guess I'm not certain how that differs from an axiom.

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:05):

I have struggled explaining it before, but I guess I'll still try

view this post on Zulip Mario Carneiro (Mar 25 2019 at 03:06):

constant never goes out of scope, it's as permanent as a def

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:06):

def f : nat -> nat := fun x, x+1 is the same as:

variable (n : nat)
def f : nat := n + 1

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:07):

but if you do:

constant n : nat
def g : nat := n + 1

then you're declaring a constant n and g is now a natural number, not a function

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:07):

f 3 evaluates to 4 while g 3 is a type mismatch because the type of g is nat

view this post on Zulip Mario Carneiro (Mar 25 2019 at 03:08):

f (f n) works but g (g n) doesn't make sense

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:08):

g n doesn't make sense to start with?

view this post on Zulip Mario Carneiro (Mar 25 2019 at 03:09):

My point being that there is no analog of f (f n) for g

view this post on Zulip Mario Carneiro (Mar 25 2019 at 03:09):

you can't substitute for a constant

view this post on Zulip Patrick Thomas (Mar 25 2019 at 03:16):

So it is like constants and variables in C? I.e. const float pi = 3.14, versus int x = 0. pi can never take a different value, but x can?

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:18):

well Lean is a functional programming language like Haskell, unlike the more conventional programming languages (C, Java, Python) which are imperative languages

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:18):

but Lean constant would be C const with a "secret" value

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:18):

where variable is just the input to functions

view this post on Zulip Patrick Thomas (Mar 25 2019 at 03:28):

I think I kind of see. I started reading a tutorial on Haskell earlier this week. Does it have something similar that I will run across?

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:30):

I don't know Haskell but I don't think so

view this post on Zulip Patrick Thomas (Mar 25 2019 at 03:37):

Is a variable the same as a variable in the lambda calculus?

view this post on Zulip Kenny Lau (Mar 25 2019 at 03:38):

yes

view this post on Zulip Patrick Thomas (Mar 25 2019 at 03:39):

Ah. I have not gotten to the typed lambda calculus yet. Will I see constants there?

view this post on Zulip Mario Carneiro (Mar 25 2019 at 03:41):

Constants are like Haskell compiler intrinsic functions

view this post on Zulip Mario Carneiro (Mar 25 2019 at 03:42):

they are functions, you can see that they have been declared as such, but you can't see the definition

view this post on Zulip Mario Carneiro (Mar 25 2019 at 03:45):

Haskell doesn't really have an equivalent to the variables command. Scopes are handled differently in Haskell - you can think of the whole program as being in a single shared scopes where all your definitions are like let bindings. Lean is not like that - there are no variable scopes that span multiple definitions

view this post on Zulip Patrick Thomas (Mar 25 2019 at 03:48):

I guess I haven't gotten that far yet.

view this post on Zulip Patrick Thomas (Mar 25 2019 at 03:49):

Are constants the same as the "term constants" mentioned here: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

view this post on Zulip Mario Carneiro (Mar 25 2019 at 05:11):

yes

view this post on Zulip Patrick Thomas (Mar 25 2019 at 05:15):

Thank you

view this post on Zulip Kevin Buzzard (Mar 25 2019 at 07:08):

One other difference is that users are hugely discouraged from ever using constants ever. I'm not sure there's a single one in mathlib. But there are variables everywhere


Last updated: May 11 2021 at 00:31 UTC