2567 binder) that are not present in Ott. Our expectation is that we can still |
2567 binder) that are not present in Ott. Our expectation is that we can still |
2568 cover many interesting term-calculi from programming language research, for |
2568 cover many interesting term-calculi from programming language research, for |
2569 example the Core-Haskell language from the Introduction. With the work |
2569 example the Core-Haskell language from the Introduction. With the work |
2570 presented in this paper we can define it formally as shown in |
2570 presented in this paper we can define it formally as shown in |
2571 Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically |
2571 Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically |
2572 a corresponding reasoning infrastructure. |
2572 a corresponding reasoning infrastructure. However we have found out that |
|
2573 telescopes seem to not easily representable in our framework. The reason is that |
|
2574 we need to be able to lift our @{text bn}-function to alpha-equated lambda-terms. |
|
2575 This requires restrictions, which class with the `global' scope of binders in |
|
2576 telescopes. They can |
|
2577 be represented in the framework desribed in \cite{WeirichYorgeySheard11} using an extension of |
|
2578 the usual locally-nameless representation. |
2573 |
2579 |
2574 \begin{figure}[p] |
2580 \begin{figure}[p] |
2575 \begin{boxedminipage}{\linewidth} |
2581 \begin{boxedminipage}{\linewidth} |
2576 \small |
2582 \small |
2577 \begin{tabular}{l} |
2583 \begin{tabular}{l} |
2677 this time by using the function package \cite{Krauss09} that has recently |
2683 this time by using the function package \cite{Krauss09} that has recently |
2678 been implemented in Isabelle/HOL and also by restricting function |
2684 been implemented in Isabelle/HOL and also by restricting function |
2679 definitions to equivariant functions (for them we can provide more |
2685 definitions to equivariant functions (for them we can provide more |
2680 automation). |
2686 automation). |
2681 |
2687 |
2682 There are some restrictions we imposed in this paper that we would like to lift in |
2688 There are some restrictions we imposed in this paper that can be lifted using |
2683 future work. One is the exclusion of nested datatype definitions. Nested |
2689 a recent reimplementation \cite{Traytel12} of the datatype package for Isabelle/HOL, which |
|
2690 is however not yet part of the stable distribution. |
|
2691 This reimplementation allows nested |
2684 datatype definitions would allow one to specify, for instance, the function kinds |
2692 datatype definitions would allow one to specify, for instance, the function kinds |
2685 in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded |
2693 in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded |
2686 version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To |
2694 version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). We can |
2687 achieve this, we need more clever implementation than we have |
2695 also use it to represent the @{text "Let"}-terms from the Introduction where |
2688 at the moment. However, really lifting this restriction will involve major |
2696 the order of @{text "let"}-assignments does not matter. This means we can represent @{text "Let"}s |
2689 work on the underlying datatype package of Isabelle/HOL. |
2697 such that the following two terms are equal |
2690 |
2698 |
2691 A more interesting line of investigation is whether we can go beyond the |
2699 \[ |
|
2700 @{text "Let x\<^isub>1 = t\<^isub>1 and x\<^isub>2 = t\<^isub>2 in s"} \;\;=\;\; |
|
2701 @{text "Let x\<^isub>2 = t\<^isub>2 and x\<^isub>1 = t\<^isub>1 in s"} |
|
2702 \]\smallskip |
|
2703 |
|
2704 \noindent |
|
2705 For this we have to represent the @{text "let"}-assignments as finite sets |
|
2706 of pair and a binding function that picks out the left components to be bound in @{text s}. |
|
2707 |
|
2708 One line of investigation is whether we can go beyond the |
2692 simple-minded form of binding functions that we adopted from Ott. At the moment, binding |
2709 simple-minded form of binding functions that we adopted from Ott. At the moment, binding |
2693 functions can only return the empty set, a singleton atom set or unions |
2710 functions can only return the empty set, a singleton atom set or unions |
2694 of atom sets (similarly for lists). It remains to be seen whether |
2711 of atom sets (similarly for lists). It remains to be seen whether |
2695 properties like |
2712 properties like |
2696 |
2713 |
2711 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many |
2728 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many |
2712 discussions about Nominal Isabelle. We thank Peter Sewell for making the |
2729 discussions about Nominal Isabelle. We thank Peter Sewell for making the |
2713 informal notes \cite{SewellBestiary} available to us and also for patiently |
2730 informal notes \cite{SewellBestiary} available to us and also for patiently |
2714 explaining some of the finer points of the Ott-tool. Stephanie Weirich |
2731 explaining some of the finer points of the Ott-tool. Stephanie Weirich |
2715 suggested to separate the subgrammars of kinds and types in our Core-Haskell |
2732 suggested to separate the subgrammars of kinds and types in our Core-Haskell |
2716 example. Ramana Kumar and Andrei Popescu helped us with comments about |
2733 example. Ramana Kumar and Andrei Popescu helped us with comments for |
2717 an earlier version of this paper. |
2734 an earlier version of this paper. |
2718 *} |
2735 *} |
2719 |
2736 |
2720 |
2737 |
2721 (*<*) |
2738 (*<*) |