Reputation
1,371
Top tag
Next privilege 2,000 Rep.
Edit questions and answers
Badges
7 10
Newest
 Yearling
Impact
~46k people reached

  • 0 posts edited
  • 0 helpful flags
  • 34 votes cast
Apr
26
comment What's the difference between recursion and corecursion?
@IoannisFilippidis we do care, at least in set theory, in that we want a specific induction principle to hold that only mentions Succ and Zero. We care how nats are used, not just how they are made. Of course, "contains" is a fuzzy concept--for example, the category of pointed sets has a "natural number object" which is a set with an element which is neither zero nor a successor. But in the usual settings the notion of "smallest" is indeed what you want. Even for old school PA if you want to be computable you only have standard models (Tennenbaum's theorem) and no bananas
Sep
3
awarded  Yearling
Apr
24
awarded  Good Answer
Jan
3
awarded  Necromancer
Sep
15
awarded  Good Answer
Sep
3
awarded  Yearling
Jun
15
comment What's the difference between recursion and corecursion?
@tathanhdinh Because omega is defined to be Succ(omega) so if Succ(y) = omega then Succ(y) = Succ(omega) and y = omega. The last step is admittedly a bit sketchy without fleshing out your foundations and formalizing the definition.
Jun
14
comment What's the difference between recursion and corecursion?
This is all a bit of lie since ocaml has value recursion I really should have used SML which is the only "mainstream"-ish language that supports inductive reasoning.
Jun
14
comment What's the difference between recursion and corecursion?
the goal is to show omega is not in nat. We do this by contradiction. If omega were in nat than the set N = nat - {omega} would satisfy the laws. That is because nat satisfies the laws. If y in N, 1. y is not omega and 2. y in nat. From 2 we know Succ(y) in nat, and by 1 y is not omega Succ(y) is not omega. Thus Succ(y) in N. N also includes zero. But, N is smaller than nat. This is a contradiction. Thus, nat does not include omega.
Dec
4
awarded  Nice Answer
Oct
3
awarded  Nice Answer
Sep
3
awarded  Yearling
Jun
5
awarded  Nice Answer
Feb
18
awarded  Caucus
Feb
5
comment Who first coined the term Higher Order Function and/or First Class Citizen?
"Higher order functions" exist in the work of Frege (functions taking functions as arguments for example), far predating Church's foundational work on the lambda calculus. A predicate in classical first oder logic is exactly a boolean valued function, so I second sclv's suggestion that this may be the source of the terminology.
Jan
4
awarded  Commentator
Jan
4
comment Why aren't user-defined operators more common?
In Haskell, parsing is "easy" (compared to most languages). Precedence is context independent. The part that gives you hard error messages is related to typeclass and advanced type system features, not to user defined operators. It is overloading, not user definition, that is the hard problem.
Dec
31
comment Why aren't user-defined operators more common?
every single one of these problems has been solved in languages that have existed for 20 years...
Dec
3
answered Why is there never any controversy regarding the switch statement?
Nov
25
revised Why is the concept of lazy evaluation useful?
deleted 5 characters in body