Comments (7)
Details: What happens is that one function (app, the way it is generated from the preprocessed version) gets lifted incorrectly, and then all of the other proofs that reference it fail. This is because the rules I have to deal with non-primitive projections in the code assume everything is fully eta-expanded, but there's a place the code isn't eta-expanding where it should be, so they don't run and app doesn't deal with non-primitive projections. Then later on proofs about app fail because projections aren't primitive.
from pumpkin-pi.
Partially fixed in a branch. The code needs to be smart enough to:
- Fully eta expand in certain places (still breaking)
- Repack all applications that result in the goal type
Fixing the second of these fixed 27/31 errors. Need to check performance and so on, and see if I can get the remaining 4. I'm not sure where the best place to repack is, generally. Non-primitive projections are annoying.
from pumpkin-pi.
2 more, so only 2 left.
These two were interesting. The SECTION/RETRACTION rules actually need to recurse too. We can think of these as recursing after vs. recursing before, I guess, but in terms of implementation there is no difference.
from pumpkin-pi.
To understand this, note that your eliminator might produce, say, a list of lists. And then in your lifted motive you'll end up with a forgotten sigT (vector (list A)). That's a nice start, but you want to make sure you lift the inner (list A) too.
from pumpkin-pi.
I set a one-day timeout for myself on this with respect to the camera ready, so unfortunately I'm going to call it with those last 2 failing cases still there. 2 is a lot better than 31. If I fix these after the camera ready and it turns out they are interesting like the last one, I'll post an errata on my website. My suspicion though is that these two are implementation errors, since they seem to revolve around mistakes in lazy eta expansion.
from pumpkin-pi.
The remaining 2 seem to be thanks to DEVOID not understand how to lift the implicit identity function when you have a hypothesis of type (list T * list T)
. Thus definitional equalities are not preserved in that case. This seems to happen with partition
, so that lifted proofs about partition
sometimes do not type check.
from pumpkin-pi.
Should check with renewed understanding of the limitations of matching and so on
from pumpkin-pi.
Related Issues (20)
- Update docs after refactor
- For refactor, rename lifting to something more descriptive
- File organization
- Generate proofs of the correctness of configurations HOT 2
- What kind of ornament relates unindexed to indexed Expr? HOT 1
- Equations integration HOT 1
- Tactic version of lifting
- Define adjunction with nicer type (cf., #68) HOT 1
- Syntax of commands feels awkward at times
- First-class lifts? First-class composition of lifts? HOT 1
- Regression bug in simplifying projections of existentials
- Merge in decompiler from PUMPKIN PATCH to master as part of "Repair" command
- Adding constructors HOT 1
- Adding hypotheses
- Revisit the positive example
- Weakening and strengthening logical predicates
- Decompiler improvements meta
- Cancel out rewrites
- Clean up code to match terminology in paper
- Combinatorial bijections?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from pumpkin-pi.