#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:
-----------------------------+----------------------------------------------
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:
#----------------------SPACE WASTING (ULAM)
SPIRAL-------------------------------------------
# 4 3 2 11
# 5 0 1 10
# 6 7 8 9
###infinite spiral in n-dim vector space which includes all existing
vectors
###in an enumerable-infinity-order, useful for autoproving n-dimensional
expressions
###by Patrick Hammer. Email: [email protected]
def existing_vectors(dim, upper_limit=-1):
r=1; inv=1; V=[0 for x in range(dim)]; step=0
while upper_limit==-1 or step<upper_limit: #upper_limit=-1 => infinite
for x in range(len(V)): #go through all dimensions
for y in range(r): #make every single step,
yield V; V[x]+=1*inv #add V before
r=r+1; inv=inv*(-1); step+=1 #increase radius, corner
reached: invert
#--------------------------------------------------------------------------------------------
#----------------------SPACE WASTING
SNAKE----------------------------------------------------
# 5 6 7 12
# 4 3 8 11
# 1 2 9 10
###infinite snake in n-dim positive integer vector space which includes
all existing
###vectors in an enumerable-infinity-order, useful for autoproving
n-dimensional
###expressions by Patrick Hammer. Email: [email protected]
def existing_vectors_positive(dim, upper_limit=-1):
r=1; inv=1; rev=false; step=0
yield [0 for x in range(dim)] #add zero vector
while upper_limit==-1 or step<upper_limit: #upper_limit=-1 =>
infinite
V=[0 for x in range(dim)]; V[0]=r #init snake on radius
for x in range(1,len(V)): #go through all
dimensions
for y in range(r): #make every single step
W=list(reversed(V)) if rev else V #add V
yield W; V[x]+=1*inv #make the step
inv=inv*(-1); #corner reached, invert
direction
for x in range(0,len(V)): #go through all
dimensions
Break=false #double loop breaker
for y in range(r+1): #make every single step
W=list(reversed(V)) if rev else V #back to the axis
yield W; V[x]+=1*inv #make the step
if(V[x]==0): Break=true #axis reached
if Break: break #double break
r=r+1; inv=inv*(-1); step+=1; rev=not rev #increase r, axis
reached: invert reversing
#---------------------------------------------------------------------------------------------
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/11828>
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.
