#11828: Existence quantor on multi-variable logic expressions for automatic
expression prooving.
-----------------------------+----------------------------------------------
Reporter: Alligadi | Owner: davidloeffler
Type: enhancement | Status: new
Priority: major | Milestone: sage-4.7.2
Component: number fields | Keywords: existence in expressions about
infinite sets
Work_issues: | Upstream: N/A
Reviewer: | Author: Patrick Hammer
Merged: | Dependencies:
-----------------------------+----------------------------------------------
Description changed by Alligadi:
Old description:
> Python already has syntax for logic.
> But existence quantor (for loop) is only possible if the set is finite,
> or one-dimensional enumerable. Many expressions about existence of
> several objects in math are based on a lot of objects from different
> infinite enumerable sets. Wouldn't it be great if true expressions like
> that could be proofed in finite time in Sage?
> That's what this ticket is about.
> I've generalized Ulam's spiral to n dimensions,
> so every integer vector in n dimensions, has a unique next vector.
>
> Examples:
> A good example not possible yet with the ZZ^n object too:
> 12 in (x*y for x in (0..) for y in (0..))
> will fail because of the order of the elements:
> (0,1)..(0,2)..(0,3)..(0,oo)
> That's where Ulam saves us all.
> any((x*y).is_prime() for x,y in ZZ^2) beeds to be extended so that it
> works like with my Ulam-Code:
> any((x*y).is_prime() for x,y in existing_vectors(dim=2))
>
> Code to fix ZZ^2 and NN^2:
> -> Attachment.
New description:
Python already has syntax for logic.
But existence quantor (for loop) is only possible if the set is finite, or
one-dimensional enumerable. Many expressions about existence of several
objects in math are based on a lot of objects from different infinite
enumerable sets. Wouldn't it be great if true expressions like that could
be proofed in finite time in Sage?
That's what this ticket is about.
I've generalized Ulam's spiral to n dimensions,
so every integer vector in n dimensions, has a unique next vector.
Examples:
A good example not possible yet with the ZZ^n object too:
12 in (x*y for x in (0..) for y in (0..))
will fail because of the order of the elements:
(0,1)..(0,2)..(0,3)..(0,oo)
That's where Ulam saves us all.
any((x*y).is_prime() for x,y in ZZ^2) beeds to be extended so that it
works like with my Ulam-Code:
any((x*y).is_prime() for x,y in existing_vectors(dim=2))
Code to fix ZZ^(2) and NN^(2):
-> Attachment.
--
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/11828#comment:2>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sage-trac?hl=en.
