Pac-man

[Jacob Thomas Errington]

Hello Idris community,

It's commonly said that Idris is pac-man complete. Having used the language to both write some simple proofs and to display some simple graphics using SDL, I can see that this is obviously true. However, has anybody actually written a Pac-man clone in Idris?

Cheers,
Jake

[David Christiansen]

No, but pac-man completeness is a corollary of space-invaders completeness, and Idris has been constructively proven to be space-invaders complete :-)

/David

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Leif Warner]

Well, it's widely assumed space-invaders completeness implies pac-man completeness - I've yet to see a formal proof that this holds for the general case, however.

[Apostolis Xekoukoulotakis]

There is an open PHD position to prove just that, if anyone is interested.

On Friday, November 4, 2016 at 9:41:29 PM UTC+2, Leif Warner wrote:

Well, it's widely assumed space-invaders completeness implies pac-man completeness - I've yet to see a formal proof that this holds for the general case, however.

On Nov 4, 2016 12:33 PM, "David Christiansen" <da...@davidchristiansen.dk> wrote:

No, but pac-man completeness is a corollary of space-invaders completeness, and Idris has been constructively proven to be space-invaders complete :-)

/David

On Nov 4, 2016 15:26, "Jacob Thomas Errington" <ja...@mail.jerrington.me> wrote:

Hello Idris community,

It's commonly said that Idris is pac-man complete. Having used the language to both write some simple proofs and to display some simple graphics using SDL, I can see that this is obviously true. However, has anybody actually written a Pac-man clone in Idris?

Cheers,
Jake

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

[Gregg Reynolds]

On Nov 4, 2016 2:41 PM, "Leif Warner" <abim...@gmail.com> wrote:
>
> Well, it's widely assumed space-invaders completeness implies pac-man completeness - I've yet to see a formal proof that this holds for the general case, however.
>

I recently saw a fascinating article on this very topic in International Journal of Pokeman Go studies.  Unfortunately I lost the link but you can google it.

>
> On Nov 4, 2016 12:33 PM, "David Christiansen" <da...@davidchristiansen.dk> wrote:
>>
>> No, but pac-man completeness is a corollary of space-invaders completeness, and Idris has been constructively proven to be space-invaders complete :-)
>>
>> /David
>>
>>
>> On Nov 4, 2016 15:26, "Jacob Thomas Errington" <ja...@mail.jerrington.me> wrote:
>>>
>>> Hello Idris community,
>>>
>>> It's commonly said that Idris is pac-man complete. Having used the language to both write some simple proofs and to display some simple graphics using SDL, I can see that this is obviously true. However, has anybody actually written a Pac-man clone in Idris?
>>>
>>> Cheers,
>>> Jake
>>>
>>> --
>>> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

>>> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

>>> For more options, visit https://groups.google.com/d/optout.
>>
>> --
>> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

>> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

>> For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

[Wiebe-Marten Wijnja]

This is very interesting!

I believe that Space Invaders and Pac-Man really are very similar on a technological level, with the differences that:

1) The original space Invaders was black/white, while Pac-Man had some colours I believe.

2) Pac-Man has a slightly more compex AI as the four ghosts all behave differently. (See: http://gameinternals.com/post/2072558330/understanding-pac-man-ghost-behavior)

This would lead me to say that Pac-Man complete is a superset of Space-Invaders complete.

Another approach, which might weirdly enough maybe be easier to prove, is to analyse the compiled assembly instructions of both games, and see how much overlap there is between these.