A Step-Indexing Approach to Partial Functions

A Step-Indexing Approach to Partial Functions

We describe an ACL2 package for defining partial recursive functions that also supports efficient execution. While packages for defining partial recursive functions already exist for other theorem provers, they often require inductive definitions or recursion operators which are not available in ACL...

Full description

Bibliographic Details
Main Authors: David Greve, Konrad Slind
Format: Article
Language:English
Published: Open Publishing Association 2013-04-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1304.7857v1
id doaj-92db4c4cdd35443bb07eae2934df1ca7
record_format Article
spelling doaj-92db4c4cdd35443bb07eae2934df1ca72020-11-25T01:16:21ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-04-01114Proc. ACL2 2013425310.4204/EPTCS.114.4A Step-Indexing Approach to Partial FunctionsDavid GreveKonrad SlindWe describe an ACL2 package for defining partial recursive functions that also supports efficient execution. While packages for defining partial recursive functions already exist for other theorem provers, they often require inductive definitions or recursion operators which are not available in ACL2 and they provide little, if any, support for executing the resulting definitions. We use step-indexing as the underlying implementation technology, enabling the definitions to be carried out in first order logic. We also show how recent enhancements to ACL2's guard feature can be used to enable the efficient execution of partial recursive functions.http://arxiv.org/pdf/1304.7857v1
collection DOAJ
language English
format Article
sources DOAJ
author David Greve
Konrad Slind
spellingShingle David Greve
Konrad Slind
A Step-Indexing Approach to Partial Functions
Electronic Proceedings in Theoretical Computer Science
author_facet David Greve
Konrad Slind
author_sort David Greve
title A Step-Indexing Approach to Partial Functions
title_short A Step-Indexing Approach to Partial Functions
title_full A Step-Indexing Approach to Partial Functions
title_fullStr A Step-Indexing Approach to Partial Functions
title_full_unstemmed A Step-Indexing Approach to Partial Functions
title_sort step-indexing approach to partial functions
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2013-04-01
description We describe an ACL2 package for defining partial recursive functions that also supports efficient execution. While packages for defining partial recursive functions already exist for other theorem provers, they often require inductive definitions or recursion operators which are not available in ACL2 and they provide little, if any, support for executing the resulting definitions. We use step-indexing as the underlying implementation technology, enabling the definitions to be carried out in first order logic. We also show how recent enhancements to ACL2's guard feature can be used to enable the efficient execution of partial recursive functions.
url http://arxiv.org/pdf/1304.7857v1
work_keys_str_mv AT davidgreve astepindexingapproachtopartialfunctions
AT konradslind astepindexingapproachtopartialfunctions
AT davidgreve stepindexingapproachtopartialfunctions
AT konradslind stepindexingapproachtopartialfunctions
_version_ 1725150076305670144

Similar Items