- About Scala
- Documentation
- Code Examples
- Software
- Scala Developers

# The Curse of DOT

Sun, 2011-07-17, 17:47

#2
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

Sun, 2011-07-17, 19:07

#3
Re: Re: The Curse of DOT

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 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?

Cheers,

Miles

--

Miles Sabin

tel: +44 7813 944 528

gtalk: miles [at] milessabin [dot] com

skype: milessabin

http://www.chuusai.com/

http://twitter.com/milessabin

Sun, 2011-07-17, 19:17

#4
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:

I've tried, but it seems no amount of beer can turn me into Martin.

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,

√

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?

Cheers,

Miles

--

Miles Sabin

tel: +44 7813 944 528

gtalk: miles [at] milessabin [dot] com

skype: milessabin

http://www.chuusai.com/

http://twitter.com/milessabin

--

Viktor Klang

Akka Tech LeadTypesafe - Enterprise-Grade Scala from the Experts

Twitter: @viktorklang

Sun, 2011-07-17, 19:27

#5
Re: Re: The Curse of DOT

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?

Cheers,

Miles

--

Miles Sabin

tel: +44 7813 944 528

gtalk: miles [at] milessabin [dot] com

skype: milessabin

http://www.chuusai.com/

http://twitter.com/milessabin

--

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

Mon, 2011-07-18, 08:47

#6
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

Mon, 2011-07-18, 08:57

#7
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

Mon, 2011-07-18, 18:17

#8
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

Mon, 2011-07-18, 18:27

#9
Re: Re: The Curse of DOT

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.

Cheers

-- Martin

Mon, 2011-07-18, 20:47

#10
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

Tue, 2011-07-19, 16:17

#11
Re: Re: The Curse of DOT

On Mon, Jul 18, 2011 at 9:46 PM, Niels <nielshoogev1 [at] gmail [dot] com> wrote:

Looking forward reading the paper.no, i was just discussing the similarities to virtual classes (wrt the challenges to proving properties of the theory, ...)

The presentation mentions virtual classes twice. Is that in the

pipeline?

more generally, these slides were not written to be consumed without me talking over them, sorry!

adriaan

Tue, 2011-07-19, 16:27

#12
Tue, 2011-07-19, 19:07

#13
Re: Re: The Curse of DOT

I couldn't find it for myself, so it's worth asking:

What does DOT stand for? :)

-0xe1a

What does DOT stand for? :)

-0xe1a

Tue, 2011-07-19, 21:27

#14
Re: Re: The Curse of DOT

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:Dependent Object Types.

What does DOT stand for? :)

Cheers

-- Martin

Wed, 2011-07-20, 00:07

#15
Re: Re: The Curse of DOT

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:Dependent Object Types.

What does DOT stand for? :)

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

Wed, 2011-07-20, 11:27

#16
Re: Re: The Curse of DOT

So where *do* I go to find out more about Deviant Old Trolls?

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 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:Dependent Object Types.

What does DOT stand for? :)

Cheers

-- Martin

Wed, 2011-07-20, 11:37

#17
Re: Re: The Curse of DOT

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:Dependent Object Types.

What does DOT stand for? :)

Cheers

-- Martin

Fri, 2011-07-22, 07:07

#18
Re: Re: The Curse of DOT

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:

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?

--

Daniel C. Sobral

I travel to the future all the time.

Fri, 2011-07-22, 07:17

#19
Re: Re: The Curse of DOT

Sorry, and the subsequent question: does not it actually mean we are

Thanks,

-Vlad

On Wed, Jul 20, 2011 at 3:30 AM, Kevin Wright <kev [dot] lee [dot] wright [at] gmail [dot] com> wrote:

*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:Dependent Object Types.

What does DOT stand for? :)

Cheers

-- Martin

Sat, 2011-07-23, 03:37

#20
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

Sat, 2011-07-23, 04:27

#21
Re: Re: The Curse of DOT

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:

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?

> Thanks,

> -Vlad

Randall Schulz

Sat, 2011-07-23, 06:27

#22
Re: Re: The Curse of DOT

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:

--

L.G. Meredith

Managing Partner

Biosimilarity LLC

7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

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 SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

Sat, 2011-07-23, 07:17

#23
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

>

Sat, 2011-07-23, 08:07

#24
Re: Re: The Curse of DOT

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>

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

>

Sat, 2011-07-23, 10:07

#25
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

>> >

>

>

Sun, 2011-07-24, 00:47

#26
Re: Re: The Curse of DOT

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>

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

>> >

>

>

On Sat, Jul 16, 2011 at 10:12 AM, Daniel Sobral <dcsobral [at] gmail [dot] com> wrote: