search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
109 stars 9 forks source link

Are the Image rules sound? [Question] #219

Closed jonsterling closed 9 years ago

jonsterling commented 9 years ago

@vrahli I was recalling the way that these were originally formulated in MetaPRL, and I remembered that for Img(A; f), they had a constraint that f not have any free variables. Details here: http://www.cin.ufpe.br/~wollic/wollic2006/nogin-kopylov-slides.pdf

Do you know why it is safe to omit this constraint in Nuprl and JonPRL?

vrahli commented 9 years ago

We still have a constraint that f is in Base. Therefore, if f has a free variable x : A, then for all a and b in A, f[x\a] has to be computationally equivalent to f[x\b].

On Thu, Aug 27, 2015 at 4:19 PM, Jonathan Sterling <notifications@github.com

wrote:

@vrahli https://github.com/vrahli I was recalling the way that these were originally formulated in MetaPRL, and I remembered that for Img(A; f), they had a constraint that f not have any free variables. Details here: http://www.cin.ufpe.br/~wollic/wollic2006/nogin-kopylov-slides.pdf

Do you know why it is safe to omit this constraint in Nuprl and JonPRL?

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/JonPRL/issues/219.

http://www.cs.cornell.edu/~rahli/

jonsterling commented 9 years ago

@vrahli Ah, perfect, thank you! What a much more elegant way of doing it.