1. Limited time only! Sign up for a free 30min personal tutor trial with Chegg Tutors
    Dismiss Notice
Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Homework Help: Program Verification - Translation rule

  1. Jan 24, 2012 #1
    Hi

    I am doing a course on Program verification and am having trouble with the properties of summation, more specifically the rule of translation:

    "Suppose function f maps values of type J to values of type K, and suppose g is a function that maps values of type K to values of type J. suppose further that f and g are inverses. That is, suppose that, for all j[itex]\in[/itex]J and k[itex]\in[/itex]K, (f.j=k) [itex]\equiv[/itex] (j=g.k)

    [itex]\left\langle[/itex] [itex]\Sigma[/itex]k[itex]\in[/itex]K:R:T[itex]\right\rangle[/itex] = [itex]\left\langle[/itex] [itex]\Sigma[/itex]j[itex]\in[/itex]J:R[k:=f.j]:T[k:=f.j][itex]\right\rangle[/itex]

    My question: I actually do not understand how the LHS of the equation equals the RHS.
    Perhaps more specifically I am not sure how R[k:=f.j] and T[k:=f.j] appears on the right side, where does it come from?
     
  2. jcsd
  3. Jan 24, 2012 #2

    Mark44

    Staff: Mentor

    Please fix your LaTeX so that it is readable. I can't tell what you're trying to say, so I can't fix it.
     
  4. Jan 25, 2012 #3
    Sorry. Here is my next attempt:

    "Suppose function f maps values of type J to values of type K, and suppose g is a function that maps values of type K to values of type J. suppose further that f and g are inverses. That is, suppose that, for all j[itex]\in[/itex]J and k[itex]\in[/itex]K, (f.j=k) [itex]\equiv[/itex] (j=g.k)

    [itex]\langle[/itex] [itex]\Sigma[/itex]k[itex]\in[/itex]K:R:T[itex]\rangle[/itex] = [itex]\langle[/itex] [itex]\Sigma[/itex]j[itex]\in[/itex]J:R[k:=f.j]:T[k:=f.j][itex]\rangle[/itex]

    My question: I actually do not understand how the LHS of the equation equals the RHS.
    Perhaps more specifically I am not sure how R[k:=f.j] and T[k:=f.j] appears on the right side, where does it come from?
     
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook




Loading...