Mixing
Relating a proof to a Haskell program
Clash Royale CLAN TAG#URR8PPP
up vote
3
down vote
favorite
I am trying to relate the following integer square root theorem
$forall x: mathbbN, exists y : mathbbN((y^2 leq x) land (x < (y+1)^2))$
and its proof to its role as a specification of the Integer Square Root isqrt ($lfloor sqrtx rfloor$) function in a Haskell program.
Below is a inductive proof of the theorem and the related Haskell program.
The proof was done using natural deduction in the Fitch system, hence there are notational differences between code and proof e.g. no $leq$ in Fitch.
For my question the details of the proof are not important. I wish to focus on the base case, and the two cases involving $exists$-Elimination and $lor$-Elimination.
I used Quickcheck as a reasonable check that the theorem holds in the code.
I can see that cases 1 and 2 in the proof correspond to the guard conditions in the Haskell definition of isqrt function. I did not specify, prove, and implement the function isqrt in any structured way. I just used any examples I could find. I believe that there must some more formal transformation from proof to code that I am missing. So despite having written both the proof and code the precise correspondence between both eludes my comprehension.
Is there a technical name for this form of proof to program relation?
I would be grateful for an explanation or pointer to the literature.
module Peano where
import Test.QuickCheck
data Nat = Z | S Nat deriving Show
-- addition
(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)
-- multiplication
(*@) :: Nat -> Nat -> Nat
x *@ Z = Z
x *@ S y = (x *@ y) +@ x
-- square
sqr x = x *@ x
-- equality
(=@) :: Nat -> Nat -> Bool
Z =@ Z = True
(S m) =@ (S n) = m =@ n
_=@ _ = False
-- lesst than
(<@) :: Nat -> Nat -> Bool
Z <@ Z = False
Z <@ x | not(x =@ Z) = True
x <@ Z | not(x =@ Z) = False
(S x) <@ (S y) = x <@ y
-- less than or equal
(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False
-- Integer square root function
isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@ (S x) = (S (isqrt x))
| (S x) <@ (sqr (S (isqrt x))) = isqrt x
-- test with Quickcheck
instance Arbitrary Nat where
arbitrary = oneof [return Z, (S <$> arbitrary) ]
isqrtPostCondition :: Nat -> Bool
isqrtPostCondition x = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.
proof-techniques correctness-proof formal-methods haskell
asked 7 hours ago
Patrick Browne
615
add a comment |Â
up vote
3
down vote
favorite
I am trying to relate the following integer square root theorem
$forall x: mathbbN, exists y : mathbbN((y^2 leq x) land (x < (y+1)^2))$
and its proof to its role as a specification of the Integer Square Root isqrt ($lfloor sqrtx rfloor$) function in a Haskell program.
Below is a inductive proof of the theorem and the related Haskell program.
The proof was done using natural deduction in the Fitch system, hence there are notational differences between code and proof e.g. no $leq$ in Fitch.
For my question the details of the proof are not important. I wish to focus on the base case, and the two cases involving $exists$-Elimination and $lor$-Elimination.
I used Quickcheck as a reasonable check that the theorem holds in the code.
I can see that cases 1 and 2 in the proof correspond to the guard conditions in the Haskell definition of isqrt function. I did not specify, prove, and implement the function isqrt in any structured way. I just used any examples I could find. I believe that there must some more formal transformation from proof to code that I am missing. So despite having written both the proof and code the precise correspondence between both eludes my comprehension.
Is there a technical name for this form of proof to program relation?
I would be grateful for an explanation or pointer to the literature.
module Peano where
import Test.QuickCheck
data Nat = Z | S Nat deriving Show
-- addition
(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)
-- multiplication
(*@) :: Nat -> Nat -> Nat
x *@ Z = Z
x *@ S y = (x *@ y) +@ x
-- square
sqr x = x *@ x
-- equality
(=@) :: Nat -> Nat -> Bool
Z =@ Z = True
(S m) =@ (S n) = m =@ n
_=@ _ = False
-- lesst than
(<@) :: Nat -> Nat -> Bool
Z <@ Z = False
Z <@ x | not(x =@ Z) = True
x <@ Z | not(x =@ Z) = False
(S x) <@ (S y) = x <@ y
-- less than or equal
(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False
-- Integer square root function
isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@ (S x) = (S (isqrt x))
| (S x) <@ (sqr (S (isqrt x))) = isqrt x
-- test with Quickcheck
instance Arbitrary Nat where
arbitrary = oneof [return Z, (S <$> arbitrary) ]
isqrtPostCondition :: Nat -> Bool
isqrtPostCondition x = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.
proof-techniques correctness-proof formal-methods haskell
asked 7 hours ago
Patrick Browne
615
add a comment |Â
up vote
3
down vote
favorite
up vote
3
down vote
favorite
I am trying to relate the following integer square root theorem
$forall x: mathbbN, exists y : mathbbN((y^2 leq x) land (x < (y+1)^2))$
and its proof to its role as a specification of the Integer Square Root isqrt ($lfloor sqrtx rfloor$) function in a Haskell program.
Below is a inductive proof of the theorem and the related Haskell program.
The proof was done using natural deduction in the Fitch system, hence there are notational differences between code and proof e.g. no $leq$ in Fitch.
For my question the details of the proof are not important. I wish to focus on the base case, and the two cases involving $exists$-Elimination and $lor$-Elimination.
I used Quickcheck as a reasonable check that the theorem holds in the code.
I can see that cases 1 and 2 in the proof correspond to the guard conditions in the Haskell definition of isqrt function. I did not specify, prove, and implement the function isqrt in any structured way. I just used any examples I could find. I believe that there must some more formal transformation from proof to code that I am missing. So despite having written both the proof and code the precise correspondence between both eludes my comprehension.
Is there a technical name for this form of proof to program relation?
I would be grateful for an explanation or pointer to the literature.
module Peano where
import Test.QuickCheck
data Nat = Z | S Nat deriving Show
-- addition
(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)
-- multiplication
(*@) :: Nat -> Nat -> Nat
x *@ Z = Z
x *@ S y = (x *@ y) +@ x
-- square
sqr x = x *@ x
-- equality
(=@) :: Nat -> Nat -> Bool
Z =@ Z = True
(S m) =@ (S n) = m =@ n
_=@ _ = False
-- lesst than
(<@) :: Nat -> Nat -> Bool
Z <@ Z = False
Z <@ x | not(x =@ Z) = True
x <@ Z | not(x =@ Z) = False
(S x) <@ (S y) = x <@ y
-- less than or equal
(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False
-- Integer square root function
isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@ (S x) = (S (isqrt x))
| (S x) <@ (sqr (S (isqrt x))) = isqrt x
-- test with Quickcheck
instance Arbitrary Nat where
arbitrary = oneof [return Z, (S <$> arbitrary) ]
isqrtPostCondition :: Nat -> Bool
isqrtPostCondition x = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.
proof-techniques correctness-proof formal-methods haskell
asked 7 hours ago
Patrick Browne
615
I am trying to relate the following integer square root theorem
$forall x: mathbbN, exists y : mathbbN((y^2 leq x) land (x < (y+1)^2))$
and its proof to its role as a specification of the Integer Square Root isqrt ($lfloor sqrtx rfloor$) function in a Haskell program.
Below is a inductive proof of the theorem and the related Haskell program.
The proof was done using natural deduction in the Fitch system, hence there are notational differences between code and proof e.g. no $leq$ in Fitch.
For my question the details of the proof are not important. I wish to focus on the base case, and the two cases involving $exists$-Elimination and $lor$-Elimination.
I used Quickcheck as a reasonable check that the theorem holds in the code.
I can see that cases 1 and 2 in the proof correspond to the guard conditions in the Haskell definition of isqrt function. I did not specify, prove, and implement the function isqrt in any structured way. I just used any examples I could find. I believe that there must some more formal transformation from proof to code that I am missing. So despite having written both the proof and code the precise correspondence between both eludes my comprehension.
Is there a technical name for this form of proof to program relation?
I would be grateful for an explanation or pointer to the literature.
module Peano where
import Test.QuickCheck
data Nat = Z | S Nat deriving Show
-- addition
(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)
-- multiplication
(*@) :: Nat -> Nat -> Nat
x *@ Z = Z
x *@ S y = (x *@ y) +@ x
-- square
sqr x = x *@ x
-- equality
(=@) :: Nat -> Nat -> Bool
Z =@ Z = True
(S m) =@ (S n) = m =@ n
_=@ _ = False
-- lesst than
(<@) :: Nat -> Nat -> Bool
Z <@ Z = False
Z <@ x | not(x =@ Z) = True
x <@ Z | not(x =@ Z) = False
(S x) <@ (S y) = x <@ y
-- less than or equal
(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False
-- Integer square root function
isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@ (S x) = (S (isqrt x))
| (S x) <@ (sqr (S (isqrt x))) = isqrt x
-- test with Quickcheck
instance Arbitrary Nat where
arbitrary = oneof [return Z, (S <$> arbitrary) ]
isqrtPostCondition :: Nat -> Bool
isqrtPostCondition x = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.
proof-techniques correctness-proof formal-methods haskell
proof-techniques correctness-proof formal-methods haskell
asked 7 hours ago
Patrick Browne
615
asked 7 hours ago
Patrick Browne
615
edited 2 hours ago
asked 7 hours ago
Patrick Browne
615
asked 7 hours ago
Patrick Browne
615
asked 7 hours ago
Patrick Browne
615
615
add a comment |Â
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
3
down vote
Your goal is to “prove†--I'm using bullets “•†for syntactic separators--
$$ ∀x ;•;; ∃y ;•;; y² ≤ x < (y+1)²$$
Proof Methods
In the natural deduction style, one proves “∀ x : ℕ • P x†by proving
two statements:
Base case :: P 0
Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function
Where, in this case,
$$P x ;;≡;; ∃y ;•; y² ≤ x < (y+1)²$$
In the constructive fashion, one proves “∃ y • Q x†by
actually finding such a $y$ using whatever data is available.
Base case
For the [base] case the input x is 0, and we need to find
some $y$ with $y² ≤ x < (y+1)²$. Clearly $y = 0$ works as shown
in the proof your posted.
Inductive step
For the [inductive] case where the input x is of the shape S a,
we need to find a $y$ with $y² ≤ S a < (y+1)²$, (*).
However, we have the assumption $P a$ which gives us a $b$ with
$b² ≤ a < (b+1)²$ --which looks really close to the goal (*).To reach our goal (*), let's do the simplest thing possible:
replace $a$ with $S a$ in (1) thereby obtaining
$b² ≤ S a < (b + 1)²$. Because of (1), and the transitivity of ≤,
the left part is true and the whole thing reduces to:
$$S a < (b + 1)²$$So if this is true, then we are done and the answer is $b$.
If it is not true, then we must have it complement:
$$(b + 1)² ≤ S a$$But from (1) we also have $a < (b + 1)² = b² + 2b + 1$
thus we obtain $S a = a + 1 < (b² + 2b + 1) + 1 ≤ b² + 4b + 2 = ((b + 1) + 1)²$Hence, we have found that $(b + 1)² ≤ S a < ((b + 1) + 1)²$
and so we may take the output $y$ to be $b + 1$ for our goal (*).
Curry-Howard: Proving ≅ Programming
The above was a proof [sketch] which corresponds to the a program.
A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$
corresponds to the program
-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0 = “the y found in the base case of the proofâ€Â
prog n = “the y found in the inductive step,
along with any conditionals and recursive callsâ€Â
Applying this to our above proof yields,
prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
in
if a + 1 <= (b + 1) * (b + 1)
then b
else b + 1
Hope that helps :-)
answered 1 hour ago
Musa Al-hassy
620147
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
3
down vote
Your goal is to “prove†--I'm using bullets “•†for syntactic separators--
$$ ∀x ;•;; ∃y ;•;; y² ≤ x < (y+1)²$$
Proof Methods
In the natural deduction style, one proves “∀ x : ℕ • P x†by proving
two statements:
Base case :: P 0
Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function
Where, in this case,
$$P x ;;≡;; ∃y ;•; y² ≤ x < (y+1)²$$
In the constructive fashion, one proves “∃ y • Q x†by
actually finding such a $y$ using whatever data is available.
Base case
For the [base] case the input x is 0, and we need to find
some $y$ with $y² ≤ x < (y+1)²$. Clearly $y = 0$ works as shown
in the proof your posted.
Inductive step
For the [inductive] case where the input x is of the shape S a,
we need to find a $y$ with $y² ≤ S a < (y+1)²$, (*).
However, we have the assumption $P a$ which gives us a $b$ with
$b² ≤ a < (b+1)²$ --which looks really close to the goal (*).To reach our goal (*), let's do the simplest thing possible:
replace $a$ with $S a$ in (1) thereby obtaining
$b² ≤ S a < (b + 1)²$. Because of (1), and the transitivity of ≤,
the left part is true and the whole thing reduces to:
$$S a < (b + 1)²$$So if this is true, then we are done and the answer is $b$.
If it is not true, then we must have it complement:
$$(b + 1)² ≤ S a$$But from (1) we also have $a < (b + 1)² = b² + 2b + 1$
thus we obtain $S a = a + 1 < (b² + 2b + 1) + 1 ≤ b² + 4b + 2 = ((b + 1) + 1)²$Hence, we have found that $(b + 1)² ≤ S a < ((b + 1) + 1)²$
and so we may take the output $y$ to be $b + 1$ for our goal (*).
Curry-Howard: Proving ≅ Programming
The above was a proof [sketch] which corresponds to the a program.
A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$
corresponds to the program
-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0 = “the y found in the base case of the proofâ€Â
prog n = “the y found in the inductive step,
along with any conditionals and recursive callsâ€Â
Applying this to our above proof yields,
prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
in
if a + 1 <= (b + 1) * (b + 1)
then b
else b + 1
Hope that helps :-)
answered 1 hour ago
Musa Al-hassy
620147
add a comment |Â
up vote
3
down vote
Your goal is to “prove†--I'm using bullets “•†for syntactic separators--
$$ ∀x ;•;; ∃y ;•;; y² ≤ x < (y+1)²$$
Proof Methods
In the natural deduction style, one proves “∀ x : ℕ • P x†by proving
two statements:
Base case :: P 0
Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function
Where, in this case,
$$P x ;;≡;; ∃y ;•; y² ≤ x < (y+1)²$$
In the constructive fashion, one proves “∃ y • Q x†by
actually finding such a $y$ using whatever data is available.
Base case
For the [base] case the input x is 0, and we need to find
some $y$ with $y² ≤ x < (y+1)²$. Clearly $y = 0$ works as shown
in the proof your posted.
Inductive step
For the [inductive] case where the input x is of the shape S a,
we need to find a $y$ with $y² ≤ S a < (y+1)²$, (*).
However, we have the assumption $P a$ which gives us a $b$ with
$b² ≤ a < (b+1)²$ --which looks really close to the goal (*).To reach our goal (*), let's do the simplest thing possible:
replace $a$ with $S a$ in (1) thereby obtaining
$b² ≤ S a < (b + 1)²$. Because of (1), and the transitivity of ≤,
the left part is true and the whole thing reduces to:
$$S a < (b + 1)²$$So if this is true, then we are done and the answer is $b$.
If it is not true, then we must have it complement:
$$(b + 1)² ≤ S a$$But from (1) we also have $a < (b + 1)² = b² + 2b + 1$
thus we obtain $S a = a + 1 < (b² + 2b + 1) + 1 ≤ b² + 4b + 2 = ((b + 1) + 1)²$Hence, we have found that $(b + 1)² ≤ S a < ((b + 1) + 1)²$
and so we may take the output $y$ to be $b + 1$ for our goal (*).
Curry-Howard: Proving ≅ Programming
The above was a proof [sketch] which corresponds to the a program.
A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$
corresponds to the program
-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0 = “the y found in the base case of the proofâ€Â
prog n = “the y found in the inductive step,
along with any conditionals and recursive callsâ€Â
Applying this to our above proof yields,
prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
in
if a + 1 <= (b + 1) * (b + 1)
then b
else b + 1
Hope that helps :-)
answered 1 hour ago
Musa Al-hassy
620147
add a comment |Â
up vote
3
down vote
up vote
3
down vote
Your goal is to “prove†--I'm using bullets “•†for syntactic separators--
$$ ∀x ;•;; ∃y ;•;; y² ≤ x < (y+1)²$$
Proof Methods
In the natural deduction style, one proves “∀ x : ℕ • P x†by proving
two statements:
Base case :: P 0
Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function
Where, in this case,
$$P x ;;≡;; ∃y ;•; y² ≤ x < (y+1)²$$
In the constructive fashion, one proves “∃ y • Q x†by
actually finding such a $y$ using whatever data is available.
Base case
For the [base] case the input x is 0, and we need to find
some $y$ with $y² ≤ x < (y+1)²$. Clearly $y = 0$ works as shown
in the proof your posted.
Inductive step
For the [inductive] case where the input x is of the shape S a,
we need to find a $y$ with $y² ≤ S a < (y+1)²$, (*).
However, we have the assumption $P a$ which gives us a $b$ with
$b² ≤ a < (b+1)²$ --which looks really close to the goal (*).To reach our goal (*), let's do the simplest thing possible:
replace $a$ with $S a$ in (1) thereby obtaining
$b² ≤ S a < (b + 1)²$. Because of (1), and the transitivity of ≤,
the left part is true and the whole thing reduces to:
$$S a < (b + 1)²$$So if this is true, then we are done and the answer is $b$.
If it is not true, then we must have it complement:
$$(b + 1)² ≤ S a$$But from (1) we also have $a < (b + 1)² = b² + 2b + 1$
thus we obtain $S a = a + 1 < (b² + 2b + 1) + 1 ≤ b² + 4b + 2 = ((b + 1) + 1)²$Hence, we have found that $(b + 1)² ≤ S a < ((b + 1) + 1)²$
and so we may take the output $y$ to be $b + 1$ for our goal (*).
Curry-Howard: Proving ≅ Programming
The above was a proof [sketch] which corresponds to the a program.
A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$
corresponds to the program
-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0 = “the y found in the base case of the proofâ€Â
prog n = “the y found in the inductive step,
along with any conditionals and recursive callsâ€Â
Applying this to our above proof yields,
prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
in
if a + 1 <= (b + 1) * (b + 1)
then b
else b + 1
Hope that helps :-)
answered 1 hour ago
Musa Al-hassy
620147
Your goal is to “prove†--I'm using bullets “•†for syntactic separators--
$$ ∀x ;•;; ∃y ;•;; y² ≤ x < (y+1)²$$
Proof Methods
In the natural deduction style, one proves “∀ x : ℕ • P x†by proving
two statements:
Base case :: P 0
Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function
Where, in this case,
$$P x ;;≡;; ∃y ;•; y² ≤ x < (y+1)²$$
In the constructive fashion, one proves “∃ y • Q x†by
actually finding such a $y$ using whatever data is available.
Base case
For the [base] case the input x is 0, and we need to find
some $y$ with $y² ≤ x < (y+1)²$. Clearly $y = 0$ works as shown
in the proof your posted.
Inductive step
For the [inductive] case where the input x is of the shape S a,
we need to find a $y$ with $y² ≤ S a < (y+1)²$, (*).
However, we have the assumption $P a$ which gives us a $b$ with
$b² ≤ a < (b+1)²$ --which looks really close to the goal (*).To reach our goal (*), let's do the simplest thing possible:
replace $a$ with $S a$ in (1) thereby obtaining
$b² ≤ S a < (b + 1)²$. Because of (1), and the transitivity of ≤,
the left part is true and the whole thing reduces to:
$$S a < (b + 1)²$$So if this is true, then we are done and the answer is $b$.
If it is not true, then we must have it complement:
$$(b + 1)² ≤ S a$$But from (1) we also have $a < (b + 1)² = b² + 2b + 1$
thus we obtain $S a = a + 1 < (b² + 2b + 1) + 1 ≤ b² + 4b + 2 = ((b + 1) + 1)²$Hence, we have found that $(b + 1)² ≤ S a < ((b + 1) + 1)²$
and so we may take the output $y$ to be $b + 1$ for our goal (*).
Curry-Howard: Proving ≅ Programming
The above was a proof [sketch] which corresponds to the a program.
A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$
corresponds to the program
-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0 = “the y found in the base case of the proofâ€Â
prog n = “the y found in the inductive step,
along with any conditionals and recursive callsâ€Â
Applying this to our above proof yields,
prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
in
if a + 1 <= (b + 1) * (b + 1)
then b
else b + 1
Hope that helps :-)
answered 1 hour ago
Musa Al-hassy
620147
answered 1 hour ago
Musa Al-hassy
620147
answered 1 hour ago
Musa Al-hassy
620147
answered 1 hour ago
Musa Al-hassy
620147
620147
add a comment |Â
add a comment |Â
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f97637%2frelating-a-proof-to-a-haskell-program%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
