Is it so that to have correct union types you already need boolean logic? (As I heard, dependent types do imply boolean logic; not sure if I have the proof around.)
Thanks, -Vlad
On Sun, Jul 17, 2011 at 7:33 AM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
I hereby have -- please note that these are ideas, not promises
On Sat, Jul 16, 2011 at 10:12 AM, Daniel Sobral <dcsobral [at] gmail [dot] com> wrote:
Adriaan, did you made the presentation available somewhere?
>>“virtualising” pattern matching (specify its zero-plus monad)
Could you, please, elaborate on this?
On Jul 17, 5:33 pm, Adriaan Moors wrote:
> I hereby have -- please note that these are ideas, not promises
>
>
>
> On Sat, Jul 16, 2011 at 10:12 AM, Daniel Sobral wrote:
> > Adriaan, did you made the presentation available somewhere?
>
> > --
> > Daniel C. Sobral
>
> > I travel to the future all the time.
>
>
>
> dot.pdf
> 172KViewDownload
Sorry, and the subsequent question: does not it actually mean we are limiting our abilities as soon as we limit ourselves with boolean logic? Not good for a general-purpose language.
Thanks, -Vlad
On Wed, Jul 20, 2011 at 3:30 AM, Kevin Wright <kev [dot] lee [dot] wright [at] gmail [dot] com> wrote:
On 20 July 2011 11:23, Chris Marshall <oxbowlakes [at] gmail [dot] com> wrote:
So where *do* I go to find out more about Deviant Old Trolls?
It sounds like you haven't had much exposure to IRC recently... The #scala channel is rather good, you know!
On Tue, Jul 19, 2011 at 9:26 PM, martin odersky <martin [dot] odersky [at] epfl [dot] ch> wrote:
On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <alex [at] cluonflux [dot] com> wrote:
I couldn't find it for myself, so it's worth asking: What does DOT stand for? :)
On Thursday 21 July 2011, Vlad Patryshev wrote:
> Sorry, and the subsequent question: does not it actually mean we are
> * limiting* our abilities as soon as we limit ourselves with boolean
> logic? Not good for a general-purpose language.
Boolean logic is simple and for deterministic state machines,
ineluctable. I.e., until we're using quantum computers, Boolean logic
is what we're working with.
How do you see it as limiting? Does the excluded middle chafe?
Dear Randall, Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic or Classical Linear Logic are all wonderful alternatives that are considerably closer to the mark of "what we're working with" when we work with computers. So, Heyting algebras and Quantales to you! ;-)
Best wishes, --greg
On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
On Thursday 21 July 2011, Vlad Patryshev wrote:
> Sorry, and the subsequent question: does not it actually mean we are
> * limiting* our abilities as soon as we limit ourselves with boolean
> logic? Not good for a general-purpose language.
Boolean logic is simple and for deterministic state machines,
ineluctable. I.e., until we're using quantum computers, Boolean logic
is what we're working with.
How do you see it as limiting? Does the excluded middle chafe?
Аctually, 2-value logic is still enough, because for any N-value
logic we can build 2-value view
with normal (false, true) values and extra predicate symbols
(This morphism will defined for each 'n-logic' value 'x', predicate
symbol(f is 'value-x'))
I.e. boolean algebra is a minimal mental structure, where we can
formalize difference between some
two things.
On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
wrote:
> Dear Randall,
> Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic or
> Classical Linear Logic are all wonderful alternatives that are considerably
> closer to the mark of "what we're working with" when we work with computers.
> So, Heyting algebras and Quantales to you! ;-)
> Best wishes,
> --greg
>
> On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz wrote:
>>
>> On Thursday 21 July 2011, Vlad Patryshev wrote:
>> > Sorry, and the subsequent question: does not it actually mean we are
>> > * limiting* our abilities as soon as we limit ourselves with boolean
>> > logic? Not good for a general-purpose language.
>>
>> Boolean logic is simple and for deterministic state machines,
>> ineluctable. I.e., until we're using quantum computers, Boolean logic
>> is what we're working with.
>>
>> How do you see it as limiting? Does the excluded middle chafe?
>>
>>
>> > Thanks,
>> > -Vlad
>>
>>
>> Randall Schulz
>
>
>
> --
> L.G. Meredith
> Managing Partner
> Biosimilarity LLC
> 7329 39th Ave SW
> Seattle, WA 98136
>
> +1 206.650.3740
>
> http://biosimilarity.blogspot.com
>
When you say "enough", I wonder, enough for what? Why is "difference between two things" so essential? Yes, the minimal logic for two logical values is a two-valued logic. But not every logic consists of values.
As to essential non-booleanness, here's an example: functions from arbitrary sets to finite sets: they do form a topos, but there's no underlying boolean topos.
Anyway, it would be curious to see how you model any intutionist logic with boolean, using predicates; any references?
Thanks, -Vlad
2011/7/22 Ruslan Shevchenko <ruslan [dot] s [dot] shevchenko [at] gmail [dot] com>
Аctually, 2-value logic is still enough, because for any N-value
logic we can build 2-value view
with normal (false, true) values and extra predicate symbols
(This morphism will defined for each 'n-logic' value 'x', predicate
symbol(f is 'value-x'))
I.e. boolean algebra is a minimal mental structure, where we can
formalize difference between some
two things.
On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
<lgreg [dot] meredith [at] gmail [dot] com> wrote:
> Dear Randall,
> Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic or
> Classical Linear Logic are all wonderful alternatives that are considerably
> closer to the mark of "what we're working with" when we work with computers.
> So, Heyting algebras and Quantales to you! ;-)
> Best wishes,
> --greg
>
> On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
>>
>> On Thursday 21 July 2011, Vlad Patryshev wrote:
>> > Sorry, and the subsequent question: does not it actually mean we are
>> > * limiting* our abilities as soon as we limit ourselves with boolean
>> > logic? Not good for a general-purpose language.
>>
>> Boolean logic is simple and for deterministic state machines,
>> ineluctable. I.e., until we're using quantum computers, Boolean logic
>> is what we're working with.
>>
>> How do you see it as limiting? Does the excluded middle chafe?
>>
>>
>> > Thanks,
>> > -Vlad
>>
>>
>> Randall Schulz
>
>
>
> --
> L.G. Meredith
> Managing Partner
> Biosimilarity LLC
> 7329 39th Ave SW
> Seattle, WA 98136
>
> +1 206.650.3740
>
> http://biosimilarity.blogspot.com
>
I see, you understand my words 'can be view as' as ' exists, mapping,
where values of non-classic logic
are mapped to boolean values'. This misunderstanding сan be causes
by my negligence in the terminology, so sorry about this,
I mean: exists mapping, where formulas of non-classic logic mapped to
formulas in classic logic'.
Simplest case is derivalbility: G |- v-(x) when value(x) is
For intutionist logic, formulas, appropriative for logical values will be:
x|- A, |- ~~A, X|- ~~~~A from one side and x|- ~A, x|- ~~~A .....
from other ;)
Links -- I will think about this during next week and may be will
write a post in blog for you when have time
(as I understand, this discussion is far from scala-language; )
2011/7/23 Vlad Patryshev :
> When you say "enough", I wonder, enough for what? Why is "difference
> between two things" so essential? Yes, the minimal logic for two logical
> values is a two-valued logic. But not every logic consists of values.
>
> As to essential non-booleanness, here's an example: functions from arbitrary
> sets to finite sets: they do form a topos, but there's no underlying boolean
> topos.
>
> Anyway, it would be curious to see how you model any intutionist logic with
> boolean, using predicates; any references?
>
> Thanks,
> -Vlad
>
>
> 2011/7/22 Ruslan Shevchenko
>>
>> Аctually, 2-value logic is still enough, because for any N-value
>> logic we can build 2-value view
>> with normal (false, true) values and extra predicate symbols
>> (This morphism will defined for each 'n-logic' value 'x', predicate
>> symbol(f is 'value-x'))
>>
>> I.e. boolean algebra is a minimal mental structure, where we can
>> formalize difference between some
>> two things.
>>
>> On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
>> wrote:
>> > Dear Randall,
>> > Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic
>> > or
>> > Classical Linear Logic are all wonderful alternatives that are
>> > considerably
>> > closer to the mark of "what we're working with" when we work with
>> > computers.
>> > So, Heyting algebras and Quantales to you! ;-)
>> > Best wishes,
>> > --greg
>> >
>> > On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz
>> > wrote:
>> >>
>> >> On Thursday 21 July 2011, Vlad Patryshev wrote:
>> >> > Sorry, and the subsequent question: does not it actually mean we are
>> >> > * limiting* our abilities as soon as we limit ourselves with boolean
>> >> > logic? Not good for a general-purpose language.
>> >>
>> >> Boolean logic is simple and for deterministic state machines,
>> >> ineluctable. I.e., until we're using quantum computers, Boolean logic
>> >> is what we're working with.
>> >>
>> >> How do you see it as limiting? Does the excluded middle chafe?
>> >>
>> >>
>> >> > Thanks,
>> >> > -Vlad
>> >>
>> >>
>> >> Randall Schulz
>> >
>> >
>> >
>> > --
>> > L.G. Meredith
>> > Managing Partner
>> > Biosimilarity LLC
>> > 7329 39th Ave SW
>> > Seattle, WA 98136
>> >
>> > +1 206.650.3740
>> >
>> > http://biosimilarity.blogspot.com
>> >
>
>
Okay, I kind of guess what you might mean. You can apply this solution to the logic of the topos I mentioned above.
Thanks, -Vlad
2011/7/23 Ruslan Shevchenko <ruslan [dot] s [dot] shevchenko [at] gmail [dot] com>
I see, you understand my words 'can be view as' as ' exists, mapping,
where values of non-classic logic
are mapped to boolean values'. This misunderstanding сan be causes
by my negligence in the terminology, so sorry about this,
I mean: exists mapping, where formulas of non-classic logic mapped to
formulas in classic logic'.
Simplest case is derivalbility: G |- v-<n>(x) when value(x) is <n>
For intutionist logic, formulas, appropriative for logical values will be:
x|- A, |- ~~A, X|- ~~~~A from one side and x|- ~A, x|- ~~~A .....
from other ;)
Links -- I will think about this during next week and may be will
write a post in blog for you when have time
(as I understand, this discussion is far from scala-language; )
2011/7/23 Vlad Patryshev <vpatryshev [at] gmail [dot] com>:
> When you say "enough", I wonder, enough for what? Why is "difference
> between two things" so essential? Yes, the minimal logic for two logical
> values is a two-valued logic. But not every logic consists of values.
>
> As to essential non-booleanness, here's an example: functions from arbitrary
> sets to finite sets: they do form a topos, but there's no underlying boolean
> topos.
>
> Anyway, it would be curious to see how you model any intutionist logic with
> boolean, using predicates; any references?
>
> Thanks,
> -Vlad
>
>
> 2011/7/22 Ruslan Shevchenko <ruslan [dot] s [dot] shevchenko [at] gmail [dot] com>
>>
>> Аctually, 2-value logic is still enough, because for any N-value
>> logic we can build 2-value view
>> with normal (false, true) values and extra predicate symbols
>> (This morphism will defined for each 'n-logic' value 'x', predicate
>> symbol(f is 'value-x'))
>>
>> I.e. boolean algebra is a minimal mental structure, where we can
>> formalize difference between some
>> two things.
>>
>> On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
>> <lgreg [dot] meredith [at] gmail [dot] com> wrote:
>> > Dear Randall,
>> > Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic
>> > or
>> > Classical Linear Logic are all wonderful alternatives that are
>> > considerably
>> > closer to the mark of "what we're working with" when we work with
>> > computers.
>> > So, Heyting algebras and Quantales to you! ;-)
>> > Best wishes,
>> > --greg
>> >
>> > On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz <rschulz [at] sonic [dot] net>
>> > wrote:
>> >>
>> >> On Thursday 21 July 2011, Vlad Patryshev wrote:
>> >> > Sorry, and the subsequent question: does not it actually mean we are
>> >> > * limiting* our abilities as soon as we limit ourselves with boolean
>> >> > logic? Not good for a general-purpose language.
>> >>
>> >> Boolean logic is simple and for deterministic state machines,
>> >> ineluctable. I.e., until we're using quantum computers, Boolean logic
>> >> is what we're working with.
>> >>
>> >> How do you see it as limiting? Does the excluded middle chafe?
>> >>
>> >>
>> >> > Thanks,
>> >> > -Vlad
>> >>
>> >>
>> >> Randall Schulz
>> >
>> >
>> >
>> > --
>> > L.G. Meredith
>> > Managing Partner
>> > Biosimilarity LLC
>> > 7329 39th Ave SW
>> > Seattle, WA 98136
>> >
>> > +1 206.650.3740
>> >
>> > http://biosimilarity.blogspot.com
>> >
>
>
I mean, Curry-Howard correspondence is between type systems and intuitionistic logic, right? Limiting it to boolean only puts constraints on types, not sure yet how to formulate it properly, but they seem to be too strict.
And, going into philosophy, I disagree with the statement that "boolean logic is what we are working with". Add time-dependency, and there's no boolean logic.
Thanks, -Vlad
On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
On Thursday 21 July 2011, Vlad Patryshev wrote:
> Sorry, and the subsequent question: does not it actually mean we are
> * limiting* our abilities as soon as we limit ourselves with boolean
> logic? Not good for a general-purpose language.
Boolean logic is simple and for deterministic state machines,
ineluctable. I.e., until we're using quantum computers, Boolean logic
is what we're working with.
How do you see it as limiting? Does the excluded middle chafe?
2011/7/19 martin odersky <martin [dot] odersky [at] epfl [dot] ch>
On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <alex [at] cluonflux [dot] com> wrote:
I couldn't find it for myself, so it's worth asking: What does DOT stand for? :)
Dependent Object Types.
Dah, that's a real fiat lux for me ! Looking only at the slides, I almost thought it was some weird name for a Scala branching, or a new compiler plug-in. So that's what it is all about ...
As for the content, it looks really promising (ok, no promise, "proposing" then), and if the intended clean-up in Scala type system is as great a success as the clean-up in Collections was, when Scala 2.8 went out, then I bet I'm going to stick to Scala for some more long and happy years.
Cheers
-- Martin
-- Alex REPAIN ENSEIRB-MATMECA - student TECHNICOLOR R&D - intern BORDEAUX I - master's student
SCALA - enthusiast
I've tried, but it seems no amount of beer can turn me into Martin.
On Sun, Jul 17, 2011 at 12:40 PM, Miles Sabin <miles [at] milessabin [dot] com> wrote:
On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
> I hereby have -- please note that these are ideas, not promises
How much beer do I have to feed you to turn them into promises?
On 17 July 2011 19:02, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
I've tried, but it seems no amount of beer can turn me into Martin.
Scotch it is then!When will you next be in the UK?
On Sun, Jul 17, 2011 at 12:40 PM, Miles Sabin <miles [at] milessabin [dot] com> wrote:
On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
> I hereby have -- please note that these are ideas, not promises
How much beer do I have to feed you to turn them into promises?
gtalk / msn : kev [dot] lee [dot] wright [at] gmail [dot] comgoogle+: http://gplus.to/thecoda kev [dot] lee [dot] wright [at] gmail [dot] commail: kevin [dot] wright [at] scalatechnology [dot] com vibe / skype: kev.lee.wright
quora: http://www.quora.com/Kevin-Wright twitter: @thecoda
"My point today is that, if we wish to count lines of code, we should not regard them as "lines produced" but as "lines spent": the current conventional wisdom is so foolish as to book that count on the wrong side of the ledger" ~ Dijkstra
Would you be able to write a blog piece about the ideas you presented?
It looks very interesting, but without some concrete examples and
explanation it looks a bit cryptic.
Niels
On Jul 18, 9:41 am, Andrew wrote:
> So, having read through the slides and spent half my time salivating,
> and the other half feeling thoroughly confused, can I ask for some
> context here?
>
> Is this something that is being actively/officially worked on? (and if
> not, why not?!? :-)
>
> Where was this presented?
>
> Ta,
> Andrew
On Mon, Jul 18, 2011 at 7:16 PM, Niels <nielshoogev1 [at] gmail [dot] com> wrote:
Adriaan,
Would you be able to write a blog piece about the ideas you presented?
It looks very interesting, but without some concrete examples and
explanation it looks a bit cryptic.
Let us get the paper done first :-) Everything else would be speculation before that is out.
The presentation mentions virtual classes twice. Is that in the
pipeline?
On Jul 18, 7:18 pm, martin odersky wrote:
> On Mon, Jul 18, 2011 at 7:16 PM, Niels wrote:
> > Adriaan,
>
> > Would you be able to write a blog piece about the ideas you presented?
> > It looks very interesting, but without some concrete examples and
> > explanation it looks a bit cryptic.
>
> Let us get the paper done first :-) Everything else would be speculation
> before that is out.
>
> Cheers
>
> -- Martin
On Mon, Jul 18, 2011 at 9:46 PM, Niels <nielshoogev1 [at] gmail [dot] com> wrote:
Looking forward reading the paper.
The presentation mentions virtual classes twice. Is that in the
pipeline?
no, i was just discussing the similarities to virtual classes (wrt the challenges to proving properties of the theory, ...) more generally, these slides were not written to be consumed without me talking over them, sorry!
adriaan
I'd like to prove this hypothesis when we meet next time.
Cheers, √
On Sun, Jul 17, 2011 at 12:40 PM, Miles Sabin <miles [at] milessabin [dot] com> wrote:
On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
> I hereby have -- please note that these are ideas, not promises
How much beer do I have to feed you to turn them into promises?
Re: The Curse of DOT
On Sat, Jul 16, 2011 at 10:12 AM, Daniel Sobral <dcsobral [at] gmail [dot] com> wrote:
Re: Re: The Curse of DOT
Thanks,
-Vlad
On Sun, Jul 17, 2011 at 7:33 AM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
Re: The Curse of DOT
>>“virtualising” pattern matching (specify its zero-plus monad)
Could you, please, elaborate on this?
On Jul 17, 5:33 pm, Adriaan Moors wrote:
> I hereby have -- please note that these are ideas, not promises
>
>
>
> On Sat, Jul 16, 2011 at 10:12 AM, Daniel Sobral wrote:
> > Adriaan, did you made the presentation available somewhere?
>
> > --
> > Daniel C. Sobral
>
> > I travel to the future all the time.
>
>
>
> dot.pdf
> 172KViewDownload
Re: Re: The Curse of DOT
On Mon, Jul 18, 2011 at 9:40 AM, xeno.by <xeno.by@gmail.com> wrote:
this is also very much work in progress -- I'll try to write up some ideas next month
adriaan
Re: Re: The Curse of DOT
What does DOT stand for? :)
-0xe1a
Re: Re: The Curse of DOT
On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <alex [at] cluonflux [dot] com> wrote:
Dependent Object Types.
Cheers
-- Martin
Re: Re: The Curse of DOT
On Tue, Jul 19, 2011 at 9:26 PM, martin odersky <martin [dot] odersky [at] epfl [dot] ch> wrote:
Re: Re: The Curse of DOT
On 20 July 2011 11:23, Chris Marshall <oxbowlakes [at] gmail [dot] com> wrote:
It sounds like you haven't had much exposure to IRC recently... The #scala channel is rather good, you know!
Re: Re: The Curse of DOT
Thanks,
-Vlad
On Wed, Jul 20, 2011 at 3:30 AM, Kevin Wright <kev [dot] lee [dot] wright [at] gmail [dot] com> wrote:
Re: Re: The Curse of DOT
On Thursday 21 July 2011, Vlad Patryshev wrote:
> Sorry, and the subsequent question: does not it actually mean we are
> * limiting* our abilities as soon as we limit ourselves with boolean
> logic? Not good for a general-purpose language.
Boolean logic is simple and for deterministic state machines,
ineluctable. I.e., until we're using quantum computers, Boolean logic
is what we're working with.
How do you see it as limiting? Does the excluded middle chafe?
> Thanks,
> -Vlad
Randall Schulz
Re: Re: The Curse of DOT
Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic or Classical Linear Logic are all wonderful alternatives that are considerably closer to the mark of "what we're working with" when we work with computers. So, Heyting algebras and Quantales to you! ;-)
Best wishes,
--greg
On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
--
L.G. Meredith
Managing Partner
Biosimilarity LLC
7329 39th Ave SWSeattle, WA 98136
+1 206.650.3740
http://biosimilarity.blogspot.com
Re: Re: The Curse of DOT
Аctually, 2-value logic is still enough, because for any N-value
logic we can build 2-value view
with normal (false, true) values and extra predicate symbols
(This morphism will defined for each 'n-logic' value 'x', predicate
symbol(f is 'value-x'))
I.e. boolean algebra is a minimal mental structure, where we can
formalize difference between some
two things.
On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
wrote:
> Dear Randall,
> Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic or
> Classical Linear Logic are all wonderful alternatives that are considerably
> closer to the mark of "what we're working with" when we work with computers.
> So, Heyting algebras and Quantales to you! ;-)
> Best wishes,
> --greg
>
> On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz wrote:
>>
>> On Thursday 21 July 2011, Vlad Patryshev wrote:
>> > Sorry, and the subsequent question: does not it actually mean we are
>> > * limiting* our abilities as soon as we limit ourselves with boolean
>> > logic? Not good for a general-purpose language.
>>
>> Boolean logic is simple and for deterministic state machines,
>> ineluctable. I.e., until we're using quantum computers, Boolean logic
>> is what we're working with.
>>
>> How do you see it as limiting? Does the excluded middle chafe?
>>
>>
>> > Thanks,
>> > -Vlad
>>
>>
>> Randall Schulz
>
>
>
> --
> L.G. Meredith
> Managing Partner
> Biosimilarity LLC
> 7329 39th Ave SW
> Seattle, WA 98136
>
> +1 206.650.3740
>
> http://biosimilarity.blogspot.com
>
Re: Re: The Curse of DOT
As to essential non-booleanness, here's an example: functions from arbitrary sets to finite sets: they do form a topos, but there's no underlying boolean topos.
Anyway, it would be curious to see how you model any intutionist logic with boolean, using predicates; any references?
Thanks,
-Vlad
2011/7/22 Ruslan Shevchenko <ruslan [dot] s [dot] shevchenko [at] gmail [dot] com>
Re: Re: The Curse of DOT
I see, you understand my words 'can be view as' as ' exists, mapping,
where values of non-classic logic
are mapped to boolean values'. This misunderstanding сan be causes
by my negligence in the terminology, so sorry about this,
I mean: exists mapping, where formulas of non-classic logic mapped to
formulas in classic logic'.
Simplest case is derivalbility: G |- v-(x) when value(x) is
For intutionist logic, formulas, appropriative for logical values will be:
x|- A, |- ~~A, X|- ~~~~A from one side and x|- ~A, x|- ~~~A .....
from other ;)
Links -- I will think about this during next week and may be will
write a post in blog for you when have time
(as I understand, this discussion is far from scala-language; )
2011/7/23 Vlad Patryshev :
> When you say "enough", I wonder, enough for what? Why is "difference
> between two things" so essential? Yes, the minimal logic for two logical
> values is a two-valued logic. But not every logic consists of values.
>
> As to essential non-booleanness, here's an example: functions from arbitrary
> sets to finite sets: they do form a topos, but there's no underlying boolean
> topos.
>
> Anyway, it would be curious to see how you model any intutionist logic with
> boolean, using predicates; any references?
>
> Thanks,
> -Vlad
>
>
> 2011/7/22 Ruslan Shevchenko
>>
>> Аctually, 2-value logic is still enough, because for any N-value
>> logic we can build 2-value view
>> with normal (false, true) values and extra predicate symbols
>> (This morphism will defined for each 'n-logic' value 'x', predicate
>> symbol(f is 'value-x'))
>>
>> I.e. boolean algebra is a minimal mental structure, where we can
>> formalize difference between some
>> two things.
>>
>> On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
>> wrote:
>> > Dear Randall,
>> > Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic
>> > or
>> > Classical Linear Logic are all wonderful alternatives that are
>> > considerably
>> > closer to the mark of "what we're working with" when we work with
>> > computers.
>> > So, Heyting algebras and Quantales to you! ;-)
>> > Best wishes,
>> > --greg
>> >
>> > On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz
>> > wrote:
>> >>
>> >> On Thursday 21 July 2011, Vlad Patryshev wrote:
>> >> > Sorry, and the subsequent question: does not it actually mean we are
>> >> > * limiting* our abilities as soon as we limit ourselves with boolean
>> >> > logic? Not good for a general-purpose language.
>> >>
>> >> Boolean logic is simple and for deterministic state machines,
>> >> ineluctable. I.e., until we're using quantum computers, Boolean logic
>> >> is what we're working with.
>> >>
>> >> How do you see it as limiting? Does the excluded middle chafe?
>> >>
>> >>
>> >> > Thanks,
>> >> > -Vlad
>> >>
>> >>
>> >> Randall Schulz
>> >
>> >
>> >
>> > --
>> > L.G. Meredith
>> > Managing Partner
>> > Biosimilarity LLC
>> > 7329 39th Ave SW
>> > Seattle, WA 98136
>> >
>> > +1 206.650.3740
>> >
>> > http://biosimilarity.blogspot.com
>> >
>
>
Re: Re: The Curse of DOT
Thanks,
-Vlad
2011/7/23 Ruslan Shevchenko <ruslan [dot] s [dot] shevchenko [at] gmail [dot] com>
Re: Re: The Curse of DOT
And, going into philosophy, I disagree with the statement that "boolean logic is what we are working with". Add time-dependency, and there's no boolean logic.
Thanks,
-Vlad
On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
Re: Re: The Curse of DOT
2011/7/19 martin odersky <martin [dot] odersky [at] epfl [dot] ch>
Dah, that's a real fiat lux for me ! Looking only at the slides, I almost thought it was some weird name for a Scala branching, or a new compiler plug-in. So that's what it is all about ...
As for the content, it looks really promising (ok, no promise, "proposing" then), and if the intended clean-up in Scala type system is as great a success as the clean-up in Collections was, when Scala 2.8 went out, then I bet I'm going to stick to Scala for some more long and happy years.
--
Alex REPAIN
ENSEIRB-MATMECA - student
TECHNICOLOR R&D - intern
BORDEAUX I - master's student
SCALA - enthusiast
Re: Re: The Curse of DOT
On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors wrote:
> I hereby have -- please note that these are ideas, not promises
How much beer do I have to feed you to turn them into promises?
Cheers,
Miles
Re: Re: The Curse of DOT
On Sun, Jul 17, 2011 at 12:40 PM, Miles Sabin <miles [at] milessabin [dot] com> wrote:
Re: Re: The Curse of DOT
On 17 July 2011 19:02, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
Scotch it is then!When will you next be in the UK?
--
Kevin Wright
gtalk / msn : kev [dot] lee [dot] wright [at] gmail [dot] comgoogle+: http://gplus.to/thecoda
kev [dot] lee [dot] wright [at] gmail [dot] commail: kevin [dot] wright [at] scalatechnology [dot] com
vibe / skype: kev.lee.wright quora: http://www.quora.com/Kevin-Wright
twitter: @thecoda
"My point today is that, if we wish to count lines of code, we should not regard them as "lines produced" but as "lines spent": the current conventional wisdom is so foolish as to book that count on the wrong side of the ledger" ~ Dijkstra
Re: The Curse of DOT
So, having read through the slides and spent half my time salivating,
and the other half feeling thoroughly confused, can I ask for some
context here?
Is this something that is being actively/officially worked on? (and if
not, why not?!? :-)
Where was this presented?
Ta,
Andrew
Re: The Curse of DOT
Adriaan,
Would you be able to write a blog piece about the ideas you presented?
It looks very interesting, but without some concrete examples and
explanation it looks a bit cryptic.
Niels
On Jul 18, 9:41 am, Andrew wrote:
> So, having read through the slides and spent half my time salivating,
> and the other half feeling thoroughly confused, can I ask for some
> context here?
>
> Is this something that is being actively/officially worked on? (and if
> not, why not?!? :-)
>
> Where was this presented?
>
> Ta,
> Andrew
Re: Re: The Curse of DOT
On Mon, Jul 18, 2011 at 7:16 PM, Niels <nielshoogev1 [at] gmail [dot] com> wrote:
Let us get the paper done first :-) Everything else would be speculation before that is out.
Cheers
-- Martin
Re: The Curse of DOT
Looking forward reading the paper.
The presentation mentions virtual classes twice. Is that in the
pipeline?
On Jul 18, 7:18 pm, martin odersky wrote:
> On Mon, Jul 18, 2011 at 7:16 PM, Niels wrote:
> > Adriaan,
>
> > Would you be able to write a blog piece about the ideas you presented?
> > It looks very interesting, but without some concrete examples and
> > explanation it looks a bit cryptic.
>
> Let us get the paper done first :-) Everything else would be speculation
> before that is out.
>
> Cheers
>
> -- Martin
Re: Re: The Curse of DOT
On Mon, Jul 18, 2011 at 9:46 PM, Niels <nielshoogev1 [at] gmail [dot] com> wrote:
no, i was just discussing the similarities to virtual classes (wrt the challenges to proving properties of the theory, ...)
more generally, these slides were not written to be consumed without me talking over them, sorry!
adriaan
Re: Re: The Curse of DOT
On Sun, Jul 17, 2011 at 8:02 PM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
So essentially what could be:
(Adriaan) => (Seq[Beer]) => (Either[Intoxication,Martin])
turned out to be
(Adriaan) => (Seq[Beer]) => (Left[Intoxication, Martin])
I'd like to prove this hypothesis when we meet next time.
Cheers,
√
--
Viktor Klang
Akka Tech LeadTypesafe - Enterprise-Grade Scala from the Experts
Twitter: @viktorklang